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