mathlib3

3250fc30 - feat(analysis/mean_inequalities, measure_theory/lp_space): extend mem_Lp.add to all p in ennreal (#5828)

feat(analysis/mean_inequalities, measure_theory/lp_space): extend mem_Lp.add to all p in ennreal (#5828) Show `(a ^ q + b ^ q) ^ (1/q) ≤ (a ^ p + b ^ p) ^ (1/p)` for `a,b : ennreal` and `0 < p <= q`. Use it to show that for `p <= 1`, if measurable functions `f` and `g` are in Lp, `f+g` is also in Lp (the case `1 <= p` is already done).