Commit 2023-06-06 13:22 ce2ed4a7

View on Github →

feat: port Analysis.Convex.Integral (#4718)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Integral.lean

added theorem ConcaveOn.average_mem_hypograph

added theorem ConcaveOn.le_map_average

added theorem ConcaveOn.le_map_integral

added theorem ConcaveOn.le_map_set_average

added theorem ConcaveOn.set_average_mem_hypograph

added theorem Convex.average_mem

added theorem Convex.average_mem_interior_of_set

added theorem Convex.integral_mem

added theorem Convex.set_average_mem

added theorem Convex.set_average_mem_closure

added theorem ConvexOn.average_mem_epigraph

added theorem ConvexOn.map_average_le

added theorem ConvexOn.map_integral_le

added theorem ConvexOn.map_set_average_le

added theorem ConvexOn.set_average_mem_epigraph

added theorem StrictConcaveOn.ae_eq_const_or_lt_map_average

added theorem StrictConvex.ae_eq_const_or_average_mem_interior

added theorem StrictConvexOn.ae_eq_const_or_map_average_lt

added theorem ae_eq_const_or_exists_average_ne_compl

added theorem ae_eq_const_or_norm_average_lt_of_norm_le_const

added theorem ae_eq_const_or_norm_integral_lt_of_norm_le_const

added theorem ae_eq_const_or_norm_set_integral_lt_of_norm_le_const