Commit 2025-04-23 03:56 089945f6

View on Github →

chore: Lintegral -> LIntegral, Laverage -> LAverage (#24282) Found during my split of MeasureTheory.Integral.Lebesgue.Basic.

Estimated changes

Modified Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean

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

Modified Mathlib/MeasureTheory/Integral/Average.lean

added theorem MeasureTheory.exists_le_setLAverage

deleted theorem MeasureTheory.exists_le_setLaverage

added theorem MeasureTheory.exists_setLAverage_le

deleted theorem MeasureTheory.exists_setLaverage_le

added theorem MeasureTheory.measure_le_setLAverage_pos

deleted theorem MeasureTheory.measure_le_setLaverage_pos

added theorem MeasureTheory.measure_mul_setLAverage

deleted theorem MeasureTheory.measure_mul_setLaverage

added theorem MeasureTheory.measure_setLAverage_le_pos

deleted theorem MeasureTheory.measure_setLaverage_le_pos

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.setLaverage_congr

deleted theorem MeasureTheory.setLaverage_congr_fun

deleted theorem MeasureTheory.setLaverage_const

deleted theorem MeasureTheory.setLaverage_eq'

deleted theorem MeasureTheory.setLaverage_eq

deleted theorem MeasureTheory.setLaverage_lt_top

deleted theorem MeasureTheory.setLaverage_one

deleted theorem MeasureTheory.setLintegral_setLaverage

added theorem MeasureTheory.toReal_setLAverage

deleted theorem MeasureTheory.toReal_setLaverage

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

added theorem MeasureTheory.setLIntegral_compl

added theorem MeasureTheory.setLIntegral_pos_iff

deleted theorem MeasureTheory.setLintegral_compl

deleted theorem MeasureTheory.setLintegral_pos_iff

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Markov.lean

added theorem MeasureTheory.measure_eq_top_of_setLIntegral_ne_top

deleted theorem MeasureTheory.measure_eq_top_of_setLintegral_ne_top

added theorem MeasureTheory.setLIntegral_eq_top_of_measure_eq_top_ne_zero

deleted theorem MeasureTheory.setLintegral_eq_top_of_measure_eq_top_ne_zero

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Sub.lean

added theorem MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable

deleted theorem MeasureTheory.exists_measurable_le_setLintegral_eq_of_integrable

added theorem MeasureTheory.exists_setLIntegral_compl_lt

deleted theorem MeasureTheory.exists_setLintegral_compl_lt