English
For a strictly convex function, with positive weights and nonconstant points, Jensen's inequality is strict.
Русский
Для строго выпуклой функции, при положительных весах и не все точки совпадают, неравенство Дженсона строго.
LaTeX
$$$ \text{StrictConvexOn}_{\mathbb{K}}(s,f) \Rightarrow f(\sum w_i p_i) < \sum w_i f(p_i)$$$
Lean4
/-- If a function `f` is convex on `s`, then the value it takes at some center of mass of points of
`s` is less than the value it takes on one of those points. -/
theorem exists_ge_of_centerMass {t : Finset ι} (h : ConvexOn 𝕜 s f) (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ t, w i)
(hp : ∀ i ∈ t, p i ∈ s) : ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i) :=
by
set y := t.centerMass w p
obtain ⟨i, hi, hfi⟩ : ∃ i ∈ {i ∈ t | w i ≠ 0}, w i • f y ≤ w i • (f ∘ p) i :=
by
have hw' : (0 : 𝕜) < ∑ i ∈ t with w i ≠ 0, w i := by rwa [sum_filter_ne_zero]
refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') ?_
rw [← sum_smul, ← smul_le_smul_iff_of_pos_left (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ← centerMass,
centerMass_filter_ne_zero]
exact h.map_centerMass_le hw₀ hw₁ hp
rw [mem_filter] at hi
exact ⟨i, hi.1, (smul_le_smul_iff_of_pos_left <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩
