Commit 2025-03-09 18:34 3ed8cd15

View on Github →

chore(MeasureTheory/Function/LpSeminorm/Basic): generalise more results to enorm classes (#22708) Cherry-picked from #21712; not exhaustive. Made as part of the Carleson project.

Estimated changes

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

modified theorem MeasureTheory.MemLp.indicator

modified theorem MeasureTheory.MemLp.left_of_add_measure

modified theorem MeasureTheory.MemLp.of_measure_le_smul

modified theorem MeasureTheory.MemLp.right_of_add_measure

modified theorem MeasureTheory.MemLp.smul_measure

modified theorem MeasureTheory.MemLp.zero'

modified theorem MeasureTheory.MemLp.zero

modified theorem MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero

modified theorem MeasureTheory.eLpNorm'_eq_zero_iff

modified theorem MeasureTheory.eLpNorm'_eq_zero_of_ae_zero'

modified theorem MeasureTheory.eLpNorm'_eq_zero_of_ae_zero

modified theorem MeasureTheory.eLpNorm'_zero'

modified theorem MeasureTheory.eLpNorm'_zero

modified theorem MeasureTheory.eLpNormEssSup_count

modified theorem MeasureTheory.eLpNormEssSup_eq_iSup

modified theorem MeasureTheory.eLpNormEssSup_eq_zero_iff

modified theorem MeasureTheory.eLpNormEssSup_indicator_const_eq

modified theorem MeasureTheory.eLpNormEssSup_indicator_const_le

modified theorem MeasureTheory.eLpNormEssSup_indicator_le

modified theorem MeasureTheory.eLpNormEssSup_smul_measure

modified theorem MeasureTheory.eLpNormEssSup_zero

modified theorem MeasureTheory.eLpNorm_enorm

modified theorem MeasureTheory.eLpNorm_eq_zero_of_ae_zero

modified theorem MeasureTheory.eLpNorm_indicator_const_le

modified theorem MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict

modified theorem MeasureTheory.eLpNorm_indicator_le

modified theorem MeasureTheory.eLpNorm_le_add_measure_left

modified theorem MeasureTheory.eLpNorm_le_add_measure_right

modified theorem MeasureTheory.eLpNorm_le_of_ae_enorm_bound

added theorem MeasureTheory.eLpNorm_mono_ae'

modified theorem MeasureTheory.eLpNorm_of_isEmpty

modified theorem MeasureTheory.eLpNorm_one_add_measure

modified theorem MeasureTheory.eLpNorm_restrict_eq_of_support_subset

modified theorem MeasureTheory.eLpNorm_smul_measure_of_ne_top'

modified theorem MeasureTheory.eLpNorm_smul_measure_of_ne_top

modified theorem MeasureTheory.eLpNorm_smul_measure_of_ne_zero'

modified theorem MeasureTheory.eLpNorm_smul_measure_of_ne_zero

modified theorem MeasureTheory.eLpNorm_zero'

modified theorem MeasureTheory.eLpNorm_zero

modified theorem MeasureTheory.memLp_indicator_iff_restrict

modified theorem MeasureTheory.memLp_measure_zero

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean