Commit 2025-03-05 16:21 20e97c36

View on Github →

feat: add enorm versions of many nnnorm lemmas (#22175) Extracted from #21433; this PR does not try to change existing lemmas, but merely adds new versions. Generalise a few lemmas to ENorm, to show that this is already useful. Part of the Carleson project.

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem enorm'_eq_iff_norm_eq

added theorem enorm'_le_iff_norm_le

added theorem enorm_enorm

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

modified theorem MeasureTheory.MemLp.ae_eq

deleted theorem MeasureTheory.coe_nnnorm_ae_le_eLpNormEssSup

modified theorem MeasureTheory.eLpNorm'_congr_ae

added theorem MeasureTheory.eLpNorm'_congr_enorm_ae

added theorem MeasureTheory.eLpNorm'_enorm

added theorem MeasureTheory.eLpNorm'_mono_enorm_ae

modified theorem MeasureTheory.eLpNorm'_norm

modified theorem MeasureTheory.eLpNormEssSup_congr_ae

added theorem MeasureTheory.eLpNormEssSup_le_of_ae_enorm_bound

added theorem MeasureTheory.eLpNormEssSup_lt_top_of_ae_enorm_bound

added theorem MeasureTheory.eLpNormEssSup_mono_enorm_ae

modified theorem MeasureTheory.eLpNorm_congr_ae

added theorem MeasureTheory.eLpNorm_congr_enorm_ae

added theorem MeasureTheory.eLpNorm_enorm

added theorem MeasureTheory.eLpNorm_le_of_ae_enorm_bound

added theorem MeasureTheory.eLpNorm_mono_enorm

added theorem MeasureTheory.eLpNorm_mono_enorm_ae

modified theorem MeasureTheory.eLpNorm_restrict_le

added theorem MeasureTheory.enorm_ae_le_eLpNormEssSup

modified theorem MeasureTheory.memLp_congr_ae

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

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean