English
Let s be a subset of a vector space and f, g be functions from the space to a ordered additive monoid, both convex on s. Then their sum f + g is convex on s.
Русский
Пусть s — подмножество векторного пространства, а функции f, g: E → β выпуклы на s. Тогда сумма f + g выпукла на s.
LaTeX
$$$ConvexOn\ 𝕜\ s\ f \land ConvexOn\ 𝕜\ s\ g \rightarrow ConvexOn\ 𝕜\ s\ (f+g)$$$
Lean4
theorem add (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) : ConvexOn 𝕜 s (f + g) :=
⟨hf.1, fun x hx y hy a b ha hb hab =>
calc
f (a • x + b • y) + g (a • x + b • y) ≤ a • f x + b • f y + (a • g x + b • g y) :=
add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
_ = a • (f x + g x) + b • (f y + g y) := by rw [smul_add, smul_add, add_add_add_comm]⟩
