Commit 2022-02-24 04:27 f6a7ad9e

View on Github →

feat(measure_theory/integral/average): define measure_theory.average (#12128) And use it to formulate Jensen's inequality. Also add Jensen's inequality for concave functions.

Estimated changes

Modified src/analysis/convex/integral.lean

added theorem concave_on.average_mem_hypograph

added theorem concave_on.le_map_average

added theorem concave_on.le_map_integral

added theorem concave_on.le_map_set_average

added theorem concave_on.set_average_mem_hypograph

added theorem convex.average_mem

added theorem convex.set_average_mem

deleted theorem convex.smul_integral_mem

added theorem convex_on.average_mem_epigraph

added theorem convex_on.map_average_le

added theorem convex_on.map_set_average_le

deleted theorem convex_on.map_smul_integral_le

added theorem convex_on.set_average_mem_epigraph

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable.to_average

Created src/measure_theory/integral/average.lean

added theorem measure_theory.average_add_measure

added theorem measure_theory.average_congr

added theorem measure_theory.average_def'

added theorem measure_theory.average_def

added theorem measure_theory.average_eq_integral

added theorem measure_theory.average_mem_open_segment_compl_self

added theorem measure_theory.average_neg

added theorem measure_theory.average_pair

added theorem measure_theory.average_union

added theorem measure_theory.average_union_mem_open_segment

added theorem measure_theory.average_union_mem_segment

added theorem measure_theory.average_zero

added theorem measure_theory.average_zero_measure

added theorem measure_theory.measure_smul_average

added theorem measure_theory.measure_smul_set_average

added theorem measure_theory.set_average_eq

Modified src/measure_theory/integral/bochner.lean

added theorem measure_theory.tendsto_integral_approx_on_of_measurable

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.is_probability_measure_smul