English
ConvexOn.map_add_sum_le expresses Jensen's inequality when one distinguished term is singled out in a sum with a fixed base value.
Русский
ConvexOn.map_add_sum_le формулирует неравенство Дженсона, когда в сумме выделяется один член со значением, заданным базой.
LaTeX
$$$\text{ConvexOn}_{\mathbb{K}}(s,f) \Rightarrow f(v\cdot q + \sum w_i p_i) \le v\cdot f(q) + \sum w_i f(p_i)$$$
Lean4
/-- Convex **Jensen's inequality** where an element plays a distinguished role. -/
theorem map_add_sum_le (hf : ConvexOn 𝕜 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) :
f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i) :=
by
let W j := Option.elim j v w
let P j := Option.elim j q p
have : f (∑ j ∈ insertNone t, W j • P j) ≤ ∑ j ∈ insertNone t, W j • f (P j) :=
hf.map_sum_le (forall_mem_insertNone.2 ⟨hv, h₀⟩) (by simpa using h₁) (forall_mem_insertNone.2 ⟨hq, hmem⟩)
simpa using this
