Commit 2021-03-14 15:45 0a16148c

View on Github →

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.

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem ae_measurable.rpow_const

added theorem ennreal.of_real_rpow_of_nonneg

added theorem ennreal.of_real_rpow_of_pos

added theorem real.abs_rpow_of_nonneg

added theorem real.norm_rpow_of_nonneg

Modified src/measure_theory/borel_space.lean

added theorem ae_measurable.pow

added theorem measurable.pow

added theorem measurable_pow

Modified src/measure_theory/lp_space.lean

modified theorem measure_theory.snorm'_norm

added theorem measure_theory.snorm'_norm_rpow

added theorem measure_theory.snorm_norm_rpow