English
Dual version: a concaveOn function satisfies a reversed inequality when adding a distinguished term.
Русский
Дуальная версия: для вогнутой функции выполняется обратное неравенство при добавлении выделенного элемента.
LaTeX
$$$\text{ConcaveOn}_{\mathbb{K}}(s,f) \Rightarrow f(v\cdot q + \sum w_i p_i) \ge v\cdot f(q) + \sum w_i f(p_i)$$$
Lean4
/-- Concave **Jensen's inequality** where an element plays a distinguished role. -/
theorem map_add_sum_le (hf : ConcaveOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : v + ∑ i ∈ t, w i = 1)
(hmem : ∀ i ∈ t, p i ∈ s) (hv : 0 ≤ v) (hq : q ∈ s) :
v • f q + ∑ i ∈ t, w i • f (p i) ≤ f (v • q + ∑ i ∈ t, w i • p i) :=
hf.dual.map_add_sum_le h₀ h₁ hmem hv hq
