Commit 2023-06-06 04:28 6c77281d

View on Github →

feat: port MeasureTheory.Integral.Average (#4709)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/Average.lean

added theorem MeasureTheory.average_add_measure

added theorem MeasureTheory.average_congr

added theorem MeasureTheory.average_const

added theorem MeasureTheory.average_eq'

added theorem MeasureTheory.average_eq

added theorem MeasureTheory.average_eq_integral

added theorem MeasureTheory.average_mem_openSegment_compl_self

added theorem MeasureTheory.average_neg

added theorem MeasureTheory.average_pair

added theorem MeasureTheory.average_union

added theorem MeasureTheory.average_union_mem_openSegment

added theorem MeasureTheory.average_union_mem_segment

added theorem MeasureTheory.average_zero

added theorem MeasureTheory.average_zero_measure

added theorem MeasureTheory.measure_smul_average

added theorem MeasureTheory.measure_smul_set_average

added theorem MeasureTheory.set_average_const

added theorem MeasureTheory.set_average_eq'

added theorem MeasureTheory.set_average_eq