triangle ineq for finite sums/prods

Stream: mathlib4

[Yakov Pechersky]

The use of iSup came up in discussing norms over lists/multisets/finsets. If not for ciSup, how should one state that the list attains the maximum norm for some element?

@[to_additive List.iSup_nnnorm_mem_map_of_ne_nil]
lemma List.iSup_mul_nnnorm_mem_map_of_ne_nil {l : List S} (hl : l ≠ []) :
    ⨆ x ∈ l, ‖x‖₊ ∈ l.map (‖·‖₊) :=
  List.iSup_mem_map_of_ne_nil _ hl

and that for a nonarchimedean norm, the norm of the sum of the list is less than the norm of that element?

lemma _root_.List.nnnorm_prod_le_iSup_nnnorm (l : List S) :
    ‖l.prod‖₊ ≤ ⨆ x ∈ l, ‖x‖₊

[David Loeffler]

Yakov Pechersky said:

The use of iSup came up in discussing norms over lists/multisets/finsets. If not for ciSup, how should one state that the list attains the maximum norm for some element?

The lemma List.iSup_mem_map_of_ne_nil was introduced by you in a recent PR, wasn't it? I'm guessing it was specifically with this application in mind. So, while it's great that you've put in the work to PR all of these lemmas, it does mean that their existence is slightly less persuasive evidence that your chosen formulation is the best or the only possible one.

[Yakov Pechersky]

Totally agreed -- that's why I'm asking about what a preferred form would look like. I'm asking the neutral question -- not motivated to use a particular form jst because I PRed lemmas that utilize it.

[David Loeffler]

An alternative formulation of your first lemma might be:

lemma List.sup_mul_nnnorm_mem_map_of_ne_nil
    {S : Type*} [NormedGroup S] [DecidableEq S] {l : List S} (hl : l ≠ []) :
    l.toFinset.sup (fun x ↦ ‖x‖₊) ∈ l.map (‖·‖₊) := sorry

This takes about 3 lines to prove, two of which are reducing to a statement about Finsets. The Finset formulation is a one-liner:

lemma Finset.sup_mul_nnnorm_mem_image_of_nonempty
    {S : Type*} [NormedGroup S] [DecidableEq S] {s : Finset S} (hs : s.Nonempty) :
    s.sup (fun x ↦ ‖x‖₊) ∈ s.image (‖·‖₊) := by
  simpa only [Finset.mem_image, eq_comm] using s.exists_mem_eq_sup hs (fun x ↦ ‖x‖₊)

[David Loeffler]

For your second lemma (about ultrametric norms), one can formulate it as

lemma nnnorm_prod_le_sup
    {ι S : Type*} [NormedCommGroup S] [DecidableEq ι] [IsUltrametricDist S]
    (s : Finset ι) (f : ι → S) : ‖∏ i ∈ s, f i‖₊ ≤ s.sup (‖f ·‖₊) := by sorry

which typechecks, and which has a 4-line proof (given the lemma norm_mul_le_max that we both just attempted to PR).

[Notification Bot]

A message was moved here from #mathlib4 > sup and inf over sets by David Loeffler.

[Notification Bot]

3 messages were moved here from #mathlib4 > sup and inf over sets by David Loeffler.

[Notification Bot]

2 messages were moved here from #mathlib4 > sup and inf over sets by David Loeffler.

[David Loeffler]

* Context *: This thread is about possible formulations for the "ultrametric triangle inequality" for finite sums / products in normed groups.