English
Canonical equality condition for Jensen's inequality with strictly convex f: equality holds iff all points are equal (in the center of mass sense).
Русский
Условие равенства в строгой выпуклой форме: равенство достигается только когда все точки равны (по центру массы).
LaTeX
$$$ \text{StrictConvexOn}_{\mathbb{K}}(s,f) \Rightarrow f(\sum w_i p_i) = \sum w_i f(p_i) \iff \forall j, p_j = \sum w_i p_i$$$
Lean4
/-- A form of the **equality case of Jensen's equality**.
For a strictly convex function `f` and positive weights `w`, if
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)`, then the points `p` are all equal.
See also `StrictConvexOn.map_sum_eq_iff`. -/
theorem eq_of_le_map_sum (hf : StrictConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1)
(hmem : ∀ i ∈ t, p i ∈ s) (h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)) :
∀ ⦃j⦄, j ∈ t → ∀ ⦃k⦄, k ∈ t → p j = p k := by by_contra!; exact h_eq.not_gt <| hf.map_sum_lt h₀ h₁ hmem this
