Commit 2025-08-04 07:19 463ee10c

View on Github →

feat(LocallyIntegrable): generalise the first half of the file to enorms (#27457)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

modified theorem MeasureTheory.LocallyIntegrable.aestronglyMeasurable

modified theorem MeasureTheory.LocallyIntegrable.indicator

modified theorem MeasureTheory.LocallyIntegrable.integrableOn_isCompact

modified theorem MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact

modified theorem MeasureTheory.LocallyIntegrable.mono

added theorem MeasureTheory.LocallyIntegrable.mono_enorm

modified def MeasureTheory.LocallyIntegrable

modified theorem MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable

added theorem MeasureTheory.LocallyIntegrableOn.enorm

modified theorem MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset

modified theorem MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact

modified theorem MeasureTheory.LocallyIntegrableOn.mono

added theorem MeasureTheory.LocallyIntegrableOn.mono_enorm

modified theorem MeasureTheory.LocallyIntegrableOn.norm

modified def MeasureTheory.LocallyIntegrableOn

modified theorem MeasureTheory.MemLp.locallyIntegrable

modified theorem MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop

added theorem MeasureTheory.locallyIntegrableOn_const_enorm

modified theorem MeasureTheory.locallyIntegrableOn_iff

modified theorem MeasureTheory.locallyIntegrableOn_zero

added theorem MeasureTheory.locallyIntegrable_const_enorm

modified theorem MeasureTheory.locallyIntegrable_finset_sum'

modified theorem MeasureTheory.locallyIntegrable_finset_sum

modified theorem MeasureTheory.locallyIntegrable_iff

modified theorem MeasureTheory.locallyIntegrable_map_homeomorph

modified theorem MeasureTheory.locallyIntegrable_zero

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

modified theorem MeasureTheory.IntegrableAtFilter.sup_iff

modified theorem MeasureTheory.integrableAtFilter_top