mathlib

b1214293 - feat(measure_theory/lp_space): extend the definition of Lp seminorm to p ennreal (#5808)

feat(measure_theory/lp_space): extend the definition of Lp seminorm to p ennreal (#5808) Rename the seminorm with real exponent to `snorm'`, introduce `snorm_ess_sup` for `L\infty`, equal to the essential supremum of the norm.