mathlib

6480bedf - chore(measure_theory/function/lp_space): add nnnorm lemmas (#19091)

chore(measure_theory/function/lp_space): add nnnorm lemmas (#19091) This also adds a `has_nnnorm (Lp E p μ)` instance, which applies more generally (without `[fact (1 ≤ p)]`) than the version derived from `Lp.normed_add_comm_group`. In general, `nnnorm` (`‖f x‖₊)` statements can often be easier to work with because there is no need to repeatedly remind Lean that the norm is non-negative. Most of the time, the `norm` (`‖x‖`) counterparts follow trivially from the `nnnorm` ones. Notably this removes the need for a proof-by-cases in `snorm_le_mul_snorm_of_ae_le_mul` and some similar lemmas.