free abelian group norm

Stream: condensed mathematics

[Johan Commelin]

There is a map free_abelian_group X → ℕ that sends ∑ a_i [x_i] to ∑ |a_i|.

[Johan Commelin]

We need a bunch of properties of this norm map. I pushed a bunch of self-contained sorries to free_abelian_exact.lean.

[Johan Commelin]

Things like norm_add : (a+b).norm ≤ a.norm + b.norm

[Johan Commelin]

I will work on

lemma norm_eq_succ_iff (n : ℕ) :
  a.norm = n.succ ↔ ∃ b x, (a = b + of x ∨ a = b - of x) ∧ b.norm = n :=

[Sebastien Gouezel]

The right to left implication is not true (if b = - of x, for instance...)

[Johan Commelin]

Yes, I just realized.

[Johan Commelin]

Luckily I don't need it :rofl:

[Johan Commelin]

Ok, the left-to-right implication is done

[Filippo A. E. Nuccio]

I am taking on the first two norm_of and norm_add

[Eric Wieser]

I wonder if this is an argument towards having an API for nat-valued norms, since @Wrenna Robson wanted one for hamming codes too.

[Filippo A. E. Nuccio]

It could be, in the meanwhile for what concerns this very file I have almost killed all sorry's.

[Eric Wieser]

Either that, or the norm in question ought to be defined as a real instead

[Eric Wieser]

(I mean this as a suggestion for a follow-up for reintegration into mathlib, not something LTE needs to care about right now)

[Johan Commelin]

I need it ℕ-valued because I want to do induction on the norm

[Eric Wieser]

You could prove the norm is equal to a casted nat and do induction on that

[Eric Wieser]

But arguably it would be cleaner to just allow arbitrary-typed norms, since then the norm on docs#free_abelian_group would just be a special case of an L1-norm on finsupp.

[Filippo A. E. Nuccio]

OK, I am done, the file is sorry-free.

[Wrenna Robson]

Yeah, nat-valued norms are useful in compsci stuff.

[Wrenna Robson]

The difficulty would be, like, presumably you'd only want to allow for one has_norm instance for a type, but then how do you signify what its value type is?

[Yaël Dillies]

has_norm the_return_type the_normed_type?

[Johan Commelin]

Sure, but what will the type of norm x be? Or do you want the return type to be an out_param? Or do you want to write norm ℝ x and norm ℕ x, etc?

[Yaël Dillies]

We already have this problem for docs#inner, right? And the answer there is "localized notation".

[Sebastien Gouezel]

Or a global notation for the real-valued norm (which is the right norm in 99% of the cases), and specialized notation like we have for nnnorm.

[Joël Riou]

(deleted)

[Eric Wieser]

I think norm ℝ x is reasonable, keeping the existing notation for the norm and nnnorm special cases

[Eric Wieser]

I think we might end up in a nasty diamond mess if we're not careful though

[Eric Wieser]

Every real-norm induces an nnreal-norm, but the nnreal-norm induced on the product won't end up defeq to the one induced from the real-norm on the product.

[Eric Wieser]

Same for nat-norms inducing both other norms

[Wrenna Robson]

You could use something a bit like that you use for linear maps, like, ||.||[N]