Addition version of `ENNReal.Lp_add_le`

Stream: Is there code for X?

[Moritz Doll]

Is there a version of docs#ENNReal.Lp_add_le that is for addition instead of sums? in general I haven't found anything that turns lemmas about sums into lemmas about additions, but that should surely exist?

[Sebastien Gouezel]

What would be the statement you're thinking of?

[Floris van Doorn]

For the last part, docs#Fintype.sum_bool is close (but you'd really prefer the version stating a + b = \sum i, Bool.rec a b i to turn a lemma about Finset.sum into a lemma about +)

[Eric Wieser]

in general I haven't found anything that turns lemmas about sums into lemmas about additions, but that should surely exist?

Usually it doesn't since often the lemma about sums is proved in terms of the addition lemma anyway

[Moritz Doll]

Sebastien Gouezel said:

What would be the statement you're thinking of?

I need this for proving the triangle inequality for ProdLp:

((edist f1 g1 + edist g1 h1) ^ p +  (edist f2 g2 + edist g2 h2) ^ p) ^ (1 / p) ≤
(edist f1 g1 ^ p + edist f2 g2 ^ p) ^ (1 / p) +  (edist g1 h1 ^ p + edist g2 h2 ^ p) ^ (1 / p)

and in Analysis.MeanInequalities I have only found the statements for sum.

[Moritz Doll]

(for https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Inner.20product.20space.20on.20.CE.B1.20.C3.97.20.CE.B2)

[Moritz Doll]

hm, maybe docs#Finset.sum_pair can help

[Moritz Doll]

Found a solution:

have := ENNReal.Lp_add_le {0,1}
  (if · = 0 then edist f.fst g.fst else edist f.snd g.snd)
  (if · = 0 then edist g.fst h.fst else edist g.snd h.snd) hp

[Eric Wieser]

This should also work:

have := ENNReal.Lp_add_le finset.univ
  (cond · (edist f.fst g.fst) (edist f.snd g.snd))
  (cond · (edist g.fst h.fst) (edist g.snd h.snd)) hp

[Yury G. Kudryashov]

You can also use Fin.sum_univ_two with ![edist f.fst g.fst, edist f.snd g.snd]