Commit 2023-07-17 01:16 44d1fd93

View on Github →

feat: Lebesgue average (#5810) Match https://github.com/leanprover-community/mathlib/pull/19199

Estimated changes

Modified Mathlib/Analysis/Convex/Integral.lean

Modified Mathlib/Data/Real/ENNReal.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

modified theorem MeasureTheory.average_const

deleted theorem MeasureTheory.average_toReal

added theorem MeasureTheory.exists_laverage_le

added theorem MeasureTheory.exists_le_laverage

added theorem MeasureTheory.exists_le_lintegral

added theorem MeasureTheory.exists_le_setLaverage

added theorem MeasureTheory.exists_lintegral_le

added theorem MeasureTheory.exists_not_mem_null_laverage_le

added theorem MeasureTheory.exists_not_mem_null_le_laverage

added theorem MeasureTheory.exists_not_mem_null_le_lintegral

added theorem MeasureTheory.exists_not_mem_null_lintegral_le

added theorem MeasureTheory.exists_setLaverage_le

added theorem MeasureTheory.laverage_add_measure

added theorem MeasureTheory.laverage_congr

added theorem MeasureTheory.laverage_const

added theorem MeasureTheory.laverage_eq'

added theorem MeasureTheory.laverage_eq

added theorem MeasureTheory.laverage_eq_lintegral

added theorem MeasureTheory.laverage_lt_top

added theorem MeasureTheory.laverage_mem_openSegment_compl_self

added theorem MeasureTheory.laverage_one

added theorem MeasureTheory.laverage_union

added theorem MeasureTheory.laverage_union_mem_openSegment

added theorem MeasureTheory.laverage_union_mem_segment

added theorem MeasureTheory.laverage_zero

added theorem MeasureTheory.laverage_zero_measure

added theorem MeasureTheory.lintegral_laverage

added theorem MeasureTheory.measure_laverage_le_pos

added theorem MeasureTheory.measure_le_laverage_pos

added theorem MeasureTheory.measure_le_lintegral_pos

added theorem MeasureTheory.measure_le_setLaverage_pos

added theorem MeasureTheory.measure_lintegral_le_pos

added theorem MeasureTheory.measure_mul_laverage

added theorem MeasureTheory.measure_mul_setLaverage

added theorem MeasureTheory.measure_setLaverage_le_pos

added theorem MeasureTheory.measure_smul_setAverage

deleted theorem MeasureTheory.measure_smul_set_average

added theorem MeasureTheory.setAverage_congr

added theorem MeasureTheory.setAverage_congr_fun

added theorem MeasureTheory.setAverage_const

added theorem MeasureTheory.setAverage_eq'

added theorem MeasureTheory.setAverage_eq

deleted theorem MeasureTheory.setAverage_setAverage

deleted theorem MeasureTheory.setAverage_setAverage_sub

deleted theorem MeasureTheory.setAverage_toReal

added theorem MeasureTheory.setIntegral_setAverage

added theorem MeasureTheory.setIntegral_setAverage_sub

added theorem MeasureTheory.setLaverage_congr

added theorem MeasureTheory.setLaverage_congr_fun

added theorem MeasureTheory.setLaverage_const

added theorem MeasureTheory.setLaverage_eq'

added theorem MeasureTheory.setLaverage_eq

added theorem MeasureTheory.setLaverage_lt_top

added theorem MeasureTheory.setLaverage_one

added theorem MeasureTheory.setLintegral_setLaverage

deleted theorem MeasureTheory.set_average_congr_set_ae

deleted theorem MeasureTheory.set_average_const

deleted theorem MeasureTheory.set_average_eq'

deleted theorem MeasureTheory.set_average_eq

added theorem MeasureTheory.toReal_laverage

added theorem MeasureTheory.toReal_setLaverage

Modified Mathlib/MeasureTheory/Integral/IntervalAverage.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.lintegral_eq_top_of_measure_eq_top_ne_zero

deleted theorem MeasureTheory.lintegral_eq_top_of_measure_eq_top_pos

added theorem MeasureTheory.lintegral_indicator_one

added theorem MeasureTheory.measure_eq_top_of_lintegral_ne_top

added theorem MeasureTheory.measure_eq_top_of_setLintegral_ne_top

added theorem MeasureTheory.setLintegral_eq_top_of_measure_eq_top_ne_zero

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

deleted theorem MeasureTheory.Set.mulIndicator_ae_eq_one

added theorem Set.mulIndicator_ae_eq_one

Modified Mathlib/Probability/Density.lean