English
Canonical equality for Jensen inequality in concave setting; equality iff the weighted points with positive weights are equal.
Русский
Каноническое равенство для выпуклого Дженсона в остатке: равенство достигается, если ненулевые точки равны между собой.
LaTeX
$$$ \text{ConcaveOn}_{\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 nonnegative 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` with nonzero
weight 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, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i :=
hf.dual.map_sum_eq_iff' h₀ h₁ hmem
