English
Canonical form: for strictly concave f, equality in Jensen's inequality for sums occurs iff all nonzero-weighted points are equal.
Русский
Для строго вогнутой функции условие равенства в суммарной форме Дженсона выполняется тогда, когда все точки с ненулыми весами равны друг другу.
LaTeX
$$$ \text{StrictConcaveOn}_{\mathbb{K}}(s,f) \Rightarrow \text{map_sum_eq_iff'}(hf, h_0, h_1, h_{mem})$$
Lean4
/-- A form of the **equality case of Jensen's equality**.
For a strictly concave 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 `StrictConcaveOn.map_sum_eq_iff`. -/
theorem eq_of_map_sum_eq (hf : StrictConcaveOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1)
(hmem : ∀ i ∈ t, p i ∈ s) (h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)) :
∀ ⦃j⦄, j ∈ t → ∀ ⦃k⦄, k ∈ t → p j = p k := by by_contra!; exact h_eq.not_gt <| hf.lt_map_sum h₀ h₁ hmem this
