Commit 2021-01-22 17:20 3250fc30

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).