Commit 2023-07-14 16:34 9e3ff9e1

View on Github →

feat: first moment method (#5326) Forward-port leanprover-community/mathlib#18731 Also sync some parentheses with the lates mathport output.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Average.lean

added theorem MeasureTheory.average_toReal

modified theorem MeasureTheory.average_zero_measure

added theorem MeasureTheory.exists_average_le

added theorem MeasureTheory.exists_integral_le

added theorem MeasureTheory.exists_le_average

added theorem MeasureTheory.exists_le_integral

added theorem MeasureTheory.exists_le_setAverage

added theorem MeasureTheory.exists_not_mem_null_average_le

added theorem MeasureTheory.exists_not_mem_null_integral_le

added theorem MeasureTheory.exists_not_mem_null_le_average

added theorem MeasureTheory.exists_not_mem_null_le_integral

added theorem MeasureTheory.exists_setAverage_le

added theorem MeasureTheory.integral_average

added theorem MeasureTheory.integral_average_sub

added theorem MeasureTheory.integral_sub_average

added theorem MeasureTheory.measure_average_le_pos

added theorem MeasureTheory.measure_integral_le_pos

added theorem MeasureTheory.measure_le_average_pos

added theorem MeasureTheory.measure_le_integral_pos

added theorem MeasureTheory.measure_le_setAverage_pos

added theorem MeasureTheory.measure_setAverage_le_pos

added theorem MeasureTheory.ofReal_average

added theorem MeasureTheory.ofReal_setAverage

added theorem MeasureTheory.setAverage_setAverage

added theorem MeasureTheory.setAverage_setAverage_sub

added theorem MeasureTheory.setAverage_sub_setAverage

added theorem MeasureTheory.setAverage_toReal

added theorem MeasureTheory.set_average_congr_set_ae