le_map_sum — Mathlib

English

For a concaveOn f on s with weights summing to 1, the sum of weights times f(p_i) is at most f of the center mass.

Русский

Для вогнутости: сумма весов на f(p_i) не больше, чем f на центр массы.

LaTeX

$$$ \text{ConcaveOn}_{\mathbb{K}}(s,f) \Rightarrow \sum w_i f(p_i) \le f\big(\sum w_i p_i\big) $$$

Lean4

/-- Concave **Jensen's inequality**, `Finset.sum` version. -/
theorem le_map_sum (hf : ConcaveOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) :
    (∑ i ∈ t, w i • f (p i)) ≤ f (∑ i ∈ t, w i • p i) :=
  ConvexOn.map_sum_le (β := βᵒᵈ) hf h₀ h₁ hmem

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