Commit 2023-12-12 14:35 5497c1ce

View on Github →

feat: Strict Jensen inequality (#8972) and equality case From PFR

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

modified theorem Finset.prod_filter_ne_one

Modified Mathlib/Analysis/Convex/Jensen.lean

added theorem ConcaveOn.map_add_sum_le

added theorem ConvexOn.map_add_sum_le

added theorem StrictConcaveOn.eq_of_map_sum_eq

added theorem StrictConcaveOn.lt_map_sum

added theorem StrictConcaveOn.map_sum_eq_iff'

added theorem StrictConcaveOn.map_sum_eq_iff

added theorem StrictConvexOn.eq_of_le_map_sum

added theorem StrictConvexOn.map_sum_eq_iff'

added theorem StrictConvexOn.map_sum_eq_iff

added theorem StrictConvexOn.map_sum_lt

Modified Mathlib/Data/Finset/Option.lean

added theorem Finset.forall_mem_eraseNone

added theorem Finset.forall_mem_insertNone

Modified Mathlib/RingTheory/HahnSeries.lean