English
Canonical equality condition for Jensen's inequality in strictly concave setting; equality iff the 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
/-- Canonical form of the **equality case of Jensen's equality**.
For a strictly concave function `f` and positive weights `w`, we have
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)` if and only if the points `p` are all equal
(and in fact all equal to their center of mass w.r.t. `w`). -/
theorem map_sum_eq_iff (hf : StrictConcaveOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1)
(hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i :=
by simpa using hf.neg.map_sum_eq_iff h₀ h₁ hmem
