English
If f and g are strictly convex on a set, then f + g is strictly convex on that set.
Русский
Если f и g строго выпуклы на некотором множестве, то сумма f+g строго выпукла на этом множестве.
LaTeX
$$$\text{If } f\text{ and } g\text{ are strictly convex on } s,\text{ then } f+g\text{ is strictly convex on } s$$$
Lean4
theorem add_convexOn (hf : StrictConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) : StrictConvexOn 𝕜 s (f + g) :=
⟨hf.1, fun x hx y hy hxy 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_lt_add_of_lt_of_le (hf.2 hx hy hxy ha hb hab) (hg.2 hx hy ha.le hb.le hab)
_ = a • (f x + g x) + b • (f y + g y) := by rw [smul_add, smul_add, add_add_add_comm]⟩
