English
For a convexOn (s,f) with weights adding to 1, the average of f at points is bounded by f at the weighted average point.
Русский
Для выпуклой функции на s, сумма весов равна 1, среднее значение f(p_i) не меньше, чем f на средневзвешенном p.
LaTeX
$$$ \text{ConvexOn}_{\mathbb{K}}(s,f) \Rightarrow f\big(\sum_{i} w_i p_i\big) \le \sum_{i} w_i f(p_i) $$$
Lean4
/-- Convex **Jensen's inequality**, `Finset.sum` version. -/
theorem map_sum_le (hf : ConvexOn 𝕜 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) := by
simpa only [centerMass, h₁, inv_one, one_smul] using hf.map_centerMass_le h₀ (h₁.symm ▸ zero_lt_one) hmem
