English
Canonical equality case for Jensen's inequality in the convex setting; equality occurs precisely when all p_i equal.
Русский
Каноническое равенство в выпуклом случае: равенство достигается, если все p_i равны между собой.
LaTeX
$$$ \text{ConvexOn}_{\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
/-- Canonical form of the **equality case of Jensen's equality**.
For a strictly convex 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 : StrictConvexOn 𝕜 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 :=
by
have hw (i) (_ : i ∈ t) : w i • p i ≠ 0 → w i ≠ 0 := by simp_all
have hw' (i) (_ : i ∈ t) : w i • f (p i) ≠ 0 → w i ≠ 0 := by simp_all
rw [← sum_filter_of_ne hw, ← sum_filter_of_ne hw', hf.map_sum_eq_iff]
· simp
· simp +contextual [(h₀ _ _).lt_iff_ne']
· rwa [sum_filter_ne_zero]
· simp +contextual [hmem _ _]
