English
If f is strictly convex, all weights are strictly positive, and the indexed points are non-constant, then Jensen's inequality is strict.
Русский
Если функция строго выпукла, веса строго положительны и точки не все равны, неравенство Дженсона строгого типа.
LaTeX
$$$\text{StrictConvexOn}_{\mathbb{K}}(s,f) \Rightarrow (\text{weights}>0) \land \text{nonconstant} \Rightarrow f(\sum w_i p_i) < \sum w_i f(p_i)$$$
Lean4
/-- Convex **strict Jensen inequality**.
If the function is strictly convex, the weights are strictly positive and the indexed family of
points is non-constant, then Jensen's inequality is strict.
See also `StrictConvexOn.map_sum_eq_iff`. -/
theorem map_sum_lt (hf : StrictConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s)
(hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) : f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i) := by
classical
obtain ⟨j, hj, k, hk, hjk⟩ := hp
have : k ∈ t.erase j := mem_erase.2 ⟨ne_of_apply_ne _ hjk.symm, hk⟩
let u := (t.erase j).erase k
have hj : j ∉ u := by simp [u]
have hk : k ∉ u := by simp [u]
have ht : t = (u.cons k hk).cons j (mem_cons.not.2 <| not_or_intro (ne_of_apply_ne _ hjk) hj) := by
simp [u, insert_erase this, insert_erase ‹j ∈ t›, *]
clear_value u
subst ht
simp only [sum_cons]
have := h₀ j <| by simp
have := h₀ k <| by simp
let c := w j + w k
have hc : w j / c + w k / c = 1 := by simp [field, c]
calc
f (w j • p j + (w k • p k + ∑ x ∈ u, w x • p x))
_ = f (c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x) :=
by
congrm f ?_
match_scalars <;> simp [field, c]
_ ≤ c • f ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • f (p x) :=
-- apply the usual Jensen's inequality w.r.t. the weighted average of the two distinguished
-- points and all the other points
(hf.convexOn.map_add_sum_le (fun i hi ↦ (h₀ _ <| by simp [hi]).le)
(by simpa [-cons_eq_insert, ← add_assoc] using h₁) (forall_of_forall_cons <| forall_of_forall_cons hmem)
(by positivity) <|
by refine hf.1 (hmem _ <| by simp) (hmem _ <| by simp) ?_ ?_ hc <;> positivity)
_ < c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x) := by
-- then apply the definition of strict convexity for the two distinguished points
gcongr; refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc <;> positivity
_ = (w j • f (p j) + w k • f (p k)) + ∑ x ∈ u, w x • f (p x) := by match_scalars <;> simp [field, c]
_ = w j • f (p j) + (w k • f (p k) + ∑ x ∈ u, w x • f (p x)) := by abel_nf
