Commit 2023-06-21 07:24 c14c8fcd

View on Github →

feat(measure_theory/integral/average): Lebesgue average (#19199) Define the Lebesgue integral version of the average of a measurable function and prove the corresponding first moment method.

Estimated changes

Modified src/data/real/ennreal.lean

Modified src/measure_theory/integral/average.lean

modified theorem measure_theory.average_const

deleted theorem measure_theory.average_to_real

added theorem measure_theory.exists_laverage_le

added theorem measure_theory.exists_le_laverage

added theorem measure_theory.exists_le_lintegral

added theorem measure_theory.exists_le_set_laverage

added theorem measure_theory.exists_lintegral_le

added theorem measure_theory.exists_not_mem_null_laverage_le

added theorem measure_theory.exists_not_mem_null_le_laverage

added theorem measure_theory.exists_not_mem_null_le_lintegral

added theorem measure_theory.exists_not_mem_null_lintegral_le

added theorem measure_theory.exists_set_laverage_le

added theorem measure_theory.laverage_add_measure

added theorem measure_theory.laverage_congr

added theorem measure_theory.laverage_const

added theorem measure_theory.laverage_eq'

added theorem measure_theory.laverage_eq

added theorem measure_theory.laverage_eq_lintegral

added theorem measure_theory.laverage_lt_top

added theorem measure_theory.laverage_mem_open_segment_compl_self

added theorem measure_theory.laverage_one

added theorem measure_theory.laverage_union

added theorem measure_theory.laverage_union_mem_open_segment

added theorem measure_theory.laverage_union_mem_segment

added theorem measure_theory.laverage_zero

added theorem measure_theory.laverage_zero_measure

added theorem measure_theory.lintegral_laverage

added theorem measure_theory.measure_laverage_le_pos

added theorem measure_theory.measure_le_laverage_pos

added theorem measure_theory.measure_le_lintegral_pos

added theorem measure_theory.measure_le_set_laverage_pos

added theorem measure_theory.measure_lintegral_le_pos

added theorem measure_theory.measure_mul_laverage

added theorem measure_theory.measure_mul_set_laverage

added theorem measure_theory.measure_set_laverage_le_pos

added theorem measure_theory.set_average_congr

added theorem measure_theory.set_average_congr_fun

deleted theorem measure_theory.set_average_congr_set_ae

deleted theorem measure_theory.set_average_to_real

added theorem measure_theory.set_laverage_congr

added theorem measure_theory.set_laverage_congr_fun

added theorem measure_theory.set_laverage_const

added theorem measure_theory.set_laverage_eq'

added theorem measure_theory.set_laverage_eq

added theorem measure_theory.set_laverage_lt_top

added theorem measure_theory.set_laverage_one

added theorem measure_theory.set_lintegral_set_laverage

added theorem measure_theory.to_real_laverage

added theorem measure_theory.to_real_set_laverage

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.lintegral_eq_top_of_measure_eq_top_ne_zero

deleted theorem measure_theory.lintegral_eq_top_of_measure_eq_top_pos

added theorem measure_theory.lintegral_indicator_one

added theorem measure_theory.measure_eq_top_of_lintegral_ne_top

added theorem measure_theory.measure_eq_top_of_set_lintegral_ne_top

added theorem measure_theory.set_lintegral_eq_top_of_measure_eq_top_ne_zero

Modified src/measure_theory/measurable_space.lean

Modified src/measure_theory/measure/measure_space_def.lean

modified theorem set.mul_indicator_ae_eq_one

Modified src/probability/density.lean