Commit 2026-08-12 13:48 53c03db6

View on Github →

feat(MeasureTheory): the average of a sum of functions (#40389) and other basic lemmas about average From MeanFourier

Estimated changes

Modified Mathlib/Analysis/Convex/Integral.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

added theorem MeasureTheory.average_add

modified theorem MeasureTheory.average_congr

added theorem MeasureTheory.average_const_mul

added theorem MeasureTheory.average_const_smul

added theorem MeasureTheory.average_count

modified theorem MeasureTheory.average_eq'

modified theorem MeasureTheory.average_eq

modified theorem MeasureTheory.average_eq_integral

added theorem MeasureTheory.average_finsetSum

added theorem MeasureTheory.average_mul_const

modified theorem MeasureTheory.average_neg

added theorem MeasureTheory.average_nonneg

added theorem MeasureTheory.average_nonneg_of_ae

added theorem MeasureTheory.average_smul_const

added theorem MeasureTheory.average_sub

modified theorem MeasureTheory.measure_smul_average

added theorem MeasureTheory.setAverage_add

modified theorem MeasureTheory.setAverage_eq'

modified theorem MeasureTheory.setAverage_eq

added theorem MeasureTheory.setAverage_finsetSum

added theorem MeasureTheory.setAverage_sub