exists_le_of_centerMass — Mathlib

English

For strictly convex f, equality in Jensen's inequality for sums occurs iff all p_i are equal.

Русский

Для строго выпуклой функции равенство в Дженсоне по суммам достигается тогда, когда все p_i равны.

LaTeX

$$$ \text{StrictConvexOn}_{\mathbb{K}}(s,f) \Rightarrow (f(\sum w_i p_i) = \sum w_i f(p_i)) \iff (\forall i,j, p_i = p_j)$$$

Lean4

/-- If a function `f` is concave on `s`, then the value it takes at some center of mass of points of
`s` is greater than the value it takes on one of those points. -/
theorem exists_le_of_centerMass {t : Finset ι} (h : ConcaveOn 𝕜 s f) (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ t, w i)
    (hp : ∀ i ∈ t, p i ∈ s) : ∃ i ∈ t, f (p i) ≤ f (t.centerMass w p) :=
  h.dual.exists_ge_of_centerMass hw₀ hw₁ hp

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