# Commit 2023-05-25 17:14 6480bedf

View on Github →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.