mathlib3

13bf7613 - feat(measure_theory/functions/lp_space): bounds on the sum of functions in L^p, p < 1, and applications (#18796)

feat(measure_theory/functions/lp_space): bounds on the sum of functions in L^p, p < 1, and applications (#18796) The `L^p` space satisfies the triangular inequality for `p ≥ 1`. We show that, for `p < 1`, it satisfies a weaker inequality (with the loss of a multiplicative constant `2^(1/p - 1)`), which is still enough for several results. This makes it possible to remove the assumptions on `p` in results on density of continuous functions.