Commit 2023-06-11 12:27 ccdbfb6e

View on Github →

feat(measure_theory/integral/set_integral): First moment method (#18731) Integrable functions are smaller/larger than their mean on a set of positive measure. We prove it for the Bochner and Lebesgue integrals.

Estimated changes

Modified src/analysis/mean_inequalities_pow.lean

Modified src/data/real/ennreal.lean

deleted theorem ennreal.div_eq_inv_mul

added theorem ennreal.to_nnreal_ne_one

added theorem ennreal.to_nnreal_ne_zero

added theorem ennreal.to_real_ne_one

added theorem ennreal.to_real_ne_zero

Modified src/measure_theory/function/l1_space.lean

modified theorem measure_theory.integrable_const

Modified src/measure_theory/integral/average.lean

added theorem measure_theory.average_to_real

added theorem measure_theory.exists_average_le

added theorem measure_theory.exists_integral_le

added theorem measure_theory.exists_le_average

added theorem measure_theory.exists_le_integral

added theorem measure_theory.exists_le_set_average

added theorem measure_theory.exists_not_mem_null_average_le

added theorem measure_theory.exists_not_mem_null_integral_le

added theorem measure_theory.exists_not_mem_null_le_average

added theorem measure_theory.exists_not_mem_null_le_integral

added theorem measure_theory.exists_set_average_le

added theorem measure_theory.integral_average

added theorem measure_theory.integral_average_sub

added theorem measure_theory.integral_sub_average

added theorem measure_theory.measure_average_le_pos

added theorem measure_theory.measure_integral_le_pos

added theorem measure_theory.measure_le_average_pos

added theorem measure_theory.measure_le_integral_pos

added theorem measure_theory.measure_le_set_average_pos

added theorem measure_theory.measure_set_average_le_pos

added theorem measure_theory.of_real_average

added theorem measure_theory.of_real_set_average

added theorem measure_theory.set_average_congr_set_ae

added theorem measure_theory.set_average_to_real

added theorem measure_theory.set_integral_set_average

added theorem measure_theory.set_integral_set_average_sub

added theorem measure_theory.set_integral_sub_set_average