Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-26 20:23 fe6ea3ec

View on Github →

feat(analysis/convex/integral): strict Jensen's inequality (#11552)

Estimated changes

Modified src/analysis/convex/integral.lean

added theorem convex.average_mem_interior_of_set

added theorem measure_theory.integrable.ae_eq_const_or_exists_average_ne_compl

added theorem strict_concave_on.ae_eq_const_or_lt_map_average

added theorem strict_convex.ae_eq_const_or_average_mem_interior

added theorem strict_convex.ae_eq_const_or_norm_integral_lt_of_norm_le_const

added theorem strict_convex_on.ae_eq_const_or_map_average_lt