English
For a convexOn f on a convex set s, the value of f at the center of mass of points p is bounded above by a suitable center mass of the values f(p_i).
Русский
Для выпуклой функции на выпуклом множестве центроид (центр массы) нагрузки p ограничивает значение f в центре массы по значениям f(p_i).
LaTeX
$$$ \text{ConvexOn}_{\mathbb{K}}(s,f) \Rightarrow f\big(t\text{centerMass}(w,p)\big) \le t\text{centerMass}(w,f\circ p) $$$
Lean4
/-- Convex **Jensen's inequality**, `Finset.centerMass` version. -/
theorem map_centerMass_le (hf : ConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : 0 < ∑ i ∈ t, w i)
(hmem : ∀ i ∈ t, p i ∈ s) : f (t.centerMass w p) ≤ t.centerMass w (f ∘ p) :=
by
have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} := fun i hi => ⟨hmem i hi, le_rfl⟩
convert (hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2 <;>
simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]
