English
Canonical equality condition for Jensen's inequality in strictly convex setting; equality iff the selected nonzero-weighted points are equal.
Русский
Каноническое равенство в условиях строгой выпуклости: равенство достигается, если ненулевые точки равны между собой.
LaTeX
$$$ \text{StrictConvexOn}_{\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 convex 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 {w : ι → 𝕜} {p : ι → E} (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, p j = ∑ i ∈ t, w i • p i :=
by
constructor
· obtain rfl | ⟨i₀, hi₀⟩ := t.eq_empty_or_nonempty
· simp
intro h_eq i hi
have H : ∀ j ∈ t, p j = p i₀ := by
intro j hj
apply hf.eq_of_le_map_sum h₀ h₁ hmem h_eq.ge hj hi₀
calc
p i = p i₀ := by rw [H _ hi]
_ = (1 : 𝕜) • p i₀ := by simp
_ = (∑ j ∈ t, w j) • p i₀ := by rw [h₁]
_ = ∑ j ∈ t, (w j • p i₀) := by rw [sum_smul]
_ = ∑ j ∈ t, (w j • p j) := by congr! 2 with j hj; rw [← H _ hj]
· intro h
have H : ∀ j ∈ t, w j • f (p j) = w j • f (∑ i ∈ t, w i • p i) :=
by
intro j hj
simp [h j hj]
rw [sum_congr rfl H, ← sum_smul, h₁, one_smul]
