Commit 2023-06-01 05:57 77ba8883

View on Github →

feat: port MeasureTheory.Function.LocallyIntegrable (#4524)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

added theorem AntioneOn.integrableOn_isCompact

added theorem Antitone.locallyIntegrable

added theorem AntitoneOn.integrableOn_of_measure_ne_top

added theorem Continuous.integrableOn_Icc

added theorem Continuous.integrableOn_Ioc

added theorem Continuous.integrableOn_uIcc

added theorem Continuous.integrableOn_uIoc

added theorem Continuous.integrable_of_hasCompactSupport

added theorem Continuous.locallyIntegrable

added theorem ContinuousOn.integrableOn_Icc

added theorem ContinuousOn.integrableOn_compact

added theorem ContinuousOn.integrableOn_uIcc

added theorem ContinuousOn.locallyIntegrableOn

added theorem MeasureTheory.Integrable.locallyIntegrable

added theorem MeasureTheory.IntegrableOn.continuousOn_mul

added theorem MeasureTheory.IntegrableOn.continuousOn_mul_of_subset

added theorem MeasureTheory.IntegrableOn.continuousOn_smul

added theorem MeasureTheory.IntegrableOn.locallyIntegrableOn

added theorem MeasureTheory.IntegrableOn.mul_continuousOn

added theorem MeasureTheory.IntegrableOn.mul_continuousOn_of_subset

added theorem MeasureTheory.IntegrableOn.smul_continuousOn

added theorem MeasureTheory.LocallyIntegrable.aestronglyMeasurable

added theorem MeasureTheory.LocallyIntegrable.indicator

added theorem MeasureTheory.LocallyIntegrable.integrableOn_isCompact

added theorem MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact

added theorem MeasureTheory.LocallyIntegrable.locallyIntegrableOn

added def MeasureTheory.LocallyIntegrable

added theorem MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable

added theorem MeasureTheory.LocallyIntegrableOn.continuousOn_mul

added theorem MeasureTheory.LocallyIntegrableOn.continuousOn_smul

added theorem MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset

added theorem MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact

added theorem MeasureTheory.LocallyIntegrableOn.mono

added theorem MeasureTheory.LocallyIntegrableOn.mul_continuousOn

added theorem MeasureTheory.LocallyIntegrableOn.norm

added theorem MeasureTheory.LocallyIntegrableOn.smul_continuousOn

added def MeasureTheory.LocallyIntegrableOn

added theorem MeasureTheory.locallyIntegrableOn_const

added theorem MeasureTheory.locallyIntegrableOn_iff

added theorem MeasureTheory.locallyIntegrableOn_iff_locallyIntegrable_restrict

added theorem MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict

added theorem MeasureTheory.locallyIntegrableOn_univ

added theorem MeasureTheory.locallyIntegrable_const

added theorem MeasureTheory.locallyIntegrable_iff

added theorem MeasureTheory.locallyIntegrable_map_homeomorph

added theorem Monotone.locallyIntegrable

added theorem MonotoneOn.integrableOn_isCompact

added theorem MonotoneOn.integrableOn_of_measure_ne_top