Commit 2023-05-25 17:14 6480bedf

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.