Commit 2025-02-04 15:53 70cd82c1

View on Github →

chore: generalise lemmas to ENorm spaces, part 1 (#21380) Extracted from #21375: these lemmas only change the assumption on the co-domain, but not any hypothesis. This continues the work started in #20121, #20122 and #21306: those PRs generalised the definitions resp. made lemma statements use the enorm. This PR starts generalising the lemmas using those definitions. This work is part of (and a necessary pre-requisite for) the Carleson project.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/IndicatorFunction.lean

added theorem enorm_indicator_le_enorm_self

added theorem enorm_indicator_le_of_subset

added theorem indicator_enorm_le_enorm_self

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

modified theorem MeasureTheory.Memℒp.aestronglyMeasurable

modified theorem MeasureTheory.Memℒp.eLpNorm_lt_top

modified theorem MeasureTheory.Memℒp.eLpNorm_ne_top

modified theorem MeasureTheory.Memℒp.mono_measure

modified theorem MeasureTheory.Memℒp.restrict

modified theorem MeasureTheory.ae_le_eLpNormEssSup

modified theorem MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup

modified theorem MeasureTheory.eLpNorm'_const

modified theorem MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure

modified theorem MeasureTheory.eLpNorm'_eq_lintegral_enorm

modified theorem MeasureTheory.eLpNorm'_exponent_zero

modified theorem MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero

modified theorem MeasureTheory.eLpNorm'_measure_zero_of_neg

modified theorem MeasureTheory.eLpNorm'_measure_zero_of_pos

modified theorem MeasureTheory.eLpNorm'_mono_measure

modified theorem MeasureTheory.eLpNorm'_smul_measure

modified theorem MeasureTheory.eLpNormEssSup_const

modified theorem MeasureTheory.eLpNormEssSup_eq_essSup_enorm

modified theorem MeasureTheory.eLpNormEssSup_measure_zero

modified theorem MeasureTheory.eLpNormEssSup_mono_measure

modified theorem MeasureTheory.eLpNormEssSup_piecewise

modified theorem MeasureTheory.eLpNorm_const'

modified theorem MeasureTheory.eLpNorm_const

modified theorem MeasureTheory.eLpNorm_eq_eLpNorm'

modified theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm

modified theorem MeasureTheory.eLpNorm_exponent_top

modified theorem MeasureTheory.eLpNorm_exponent_zero

modified theorem MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top

modified theorem MeasureTheory.eLpNorm_measure_zero

modified theorem MeasureTheory.eLpNorm_mono_measure

modified theorem MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'

modified theorem MeasureTheory.eLpNorm_nnreal_eq_lintegral

modified theorem MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral

modified theorem MeasureTheory.eLpNorm_one_eq_lintegral_enorm

modified theorem MeasureTheory.eLpNorm_top_piecewise

modified theorem MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm'

modified theorem MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top

modified theorem MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top

modified theorem MeasureTheory.meas_eLpNormEssSup_lt

modified theorem MeasureTheory.memℒp_measure_zero

modified theorem MeasureTheory.memℒp_zero_iff_aestronglyMeasurable