mathlib3

d2d14e72 - chore(measure_theory/function/lp_space): add and reorder monotonicity results (#19092)

chore(measure_theory/function/lp_space): add and reorder monotonicity results (#19092) In #19083, I generalize the normed_space results to work without a tight bound. This is much easier if I have the more general monotonicity results available first. The `snorm'_le_nnreal_smul_snorm'_of_ae_le_mul` and `snorm_ess_sup_le_nnreal_smul_snorm_ess_sup_of_ae_le_mul` lemmas are new, and the `snorm_le_nnreal_smul_snorm_of_ae_le_mul` lemma has been adjusted to not rely on `snorm_const_smul`. All the other lemmas have just been reordered.