Commit 2022-10-03 17:40 b40ce7d0

View on Github →

feat(measure_theory/integral/average): average of constant functions (#16776) Also make the API more coherent, by renaming average_def' to average_eq to match set_average_eq. And rename lintegral_to_real_le_lintegral_nnnorm to lintegral_of_real_le_lintegral_nnnorm.

Estimated changes

Modified src/analysis/convex/integral.lean

Modified src/analysis/normed/group/basic.lean

added theorem nnnorm_sub_le

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable_inv_smul_measure

Modified src/measure_theory/integral/average.lean

added theorem measure_theory.average_const

deleted theorem measure_theory.average_def'

deleted theorem measure_theory.average_def

added theorem measure_theory.average_eq'

added theorem measure_theory.average_eq

added theorem measure_theory.set_average_const

added theorem measure_theory.set_average_eq'

Modified src/measure_theory/integral/integrable_on.lean

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.lintegral_of_real_le_lintegral_nnnorm

deleted theorem measure_theory.lintegral_to_real_le_lintegral_nnnorm