le_map_centerMass — Mathlib

English

For a concaveOn f on s, the center mass inequality reverses: the center mass value is at least the center mass of the values.

Русский

Для вогнутой функции на s неравенство центр массы обращается наоборот: значение в центре массы не меньше центра массы значений.

LaTeX

$$$ \text{ConcaveOn}_{\mathbb{K}}(s,f) \Rightarrow f( t\text{centerMass}(w,p) ) \ge t\text{centerMass}(w,f\circ p) $$$

Lean4

/-- Concave **Jensen's inequality**, `Finset.centerMass` version. -/
theorem le_map_centerMass (hf : ConcaveOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : 0 < ∑ i ∈ t, w i)
    (hmem : ∀ i ∈ t, p i ∈ s) : t.centerMass w (f ∘ p) ≤ f (t.centerMass w p) :=
  ConvexOn.map_centerMass_le (β := βᵒᵈ) hf h₀ h₁ hmem

Похожие утверждения