Commit 2025-05-06 16:26 01d39ae1

View on Github →

feat(LpSeminorm/Basic): generalise further lemmas to enorms (#24356) Continuation of #24355. In passing, we slightly tweak some typeclass assumptions:

a few lemmas (which accidentally had stronger than necessary assumptions) get weaker assumptions,
a few other lemmas have hypotheses strengthened from [ENorm E] [TopologicalSpace E] to [TopologicalSpace E] [ContinuousENorm E]. I believe this to be inconsequential, as I know no example where this distinction would matter.

Estimated changes

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

added theorem MeasureTheory.MemLp.congr_enorm

added theorem MeasureTheory.MemLp.enorm

modified theorem MeasureTheory.MemLp.left_of_add_measure

added theorem MeasureTheory.MemLp.mono'_enorm

modified theorem MeasureTheory.MemLp.mono_measure

added theorem MeasureTheory.MemLp.of_enorm_bound

modified theorem MeasureTheory.MemLp.of_enorm_le_mul

added theorem MeasureTheory.MemLp.of_le_enorm

modified theorem MeasureTheory.MemLp.of_le_mul'

modified theorem MeasureTheory.MemLp.restrict

modified theorem MeasureTheory.MemLp.right_of_add_measure

modified theorem MeasureTheory.eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul

modified theorem MeasureTheory.eLpNorm_eq_zero_iff

modified theorem MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul''

added theorem MeasureTheory.memLp_congr_enorm

added theorem MeasureTheory.memLp_enorm_iff

added theorem MeasureTheory.memLp_top_of_bound_enorm