mathlib

0a16148c - feat(measure_theory/lp_space): add snorm_norm_rpow (#6619)

feat(measure_theory/lp_space): add snorm_norm_rpow (#6619) The lemma `snorm_norm_rpow` states `snorm (λ x, ∥f x∥ ^ q) p μ = (snorm f (p * ennreal.of_real q) μ) ^ q`. Also add measurability lemmas about pow/rpow.