English
Canonical form of equality case for Jensen's equality for strictly concave/convex functions; equality holds iff the points are all equal.
Русский
Каноническая форма равенства условий Дженсона: равенство достигается только если все точки равны между собой.
LaTeX
$$$ \text{map_sum_eq_iff}(hf, h_0, h_1, h_{mem}) \iff \forall j\in t, p_j = \sum_i w_i p_i $$$
Lean4
/-- Concave **strict Jensen inequality**.
If the function is strictly concave, the weights are strictly positive and the indexed family of
points is non-constant, then Jensen's inequality is strict.
See also `StrictConcaveOn.map_sum_eq_iff`. -/
theorem lt_map_sum (hf : StrictConcaveOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i) (h₁ : ∑ i ∈ t, w i = 1)
(hmem : ∀ i ∈ t, p i ∈ s) (hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) : ∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, w i • p i) :=
hf.dual.map_sum_lt h₀ h₁ hmem hp
