Commit 2023-09-08 09:40 9f97ec19

View on Github →

feat: expand API on locally integrable functions (#7006) Measure theory prerequisites for Rademacher theorem in #7003.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

added theorem MeasureTheory.Measure.ae_prod_mem_iff_ae_ae_mem

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

added theorem MeasureTheory.Memℒp.locallyIntegrable

added theorem MeasureTheory.locallyIntegrableOn_zero

added theorem MeasureTheory.locallyIntegrable_finset_sum'

added theorem MeasureTheory.locallyIntegrable_finset_sum

added theorem MeasureTheory.locallyIntegrable_zero

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem MeasureTheory.Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top

Modified Mathlib/MeasureTheory/Group/Measure.lean

added theorem ContinuousLinearEquiv.isAddHaarMeasure_map

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean

added theorem MeasureTheory.Measure.absolutelyContinuous_isHaarMeasure