Commit 2023-04-17 16:24 13bf7613

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.