English
The pointwise maximum of two convex functions is convex.
Русский
Точечная максимума двух выпуклых функций выпукла.
LaTeX
$$$\text{If } f,g\text{ are convex on } s,\; f\lor g\text{ is convex on } s$$$
Lean4
/-- The pointwise maximum of convex functions is convex. -/
theorem sup (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) : ConvexOn 𝕜 s (f ⊔ g) :=
by
refine ⟨hf.left, fun x hx y hy a b ha hb hab => sup_le ?_ ?_⟩
·
calc
f (a • x + b • y) ≤ a • f x + b • f y := hf.right hx hy ha hb hab
_ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_left
·
calc
g (a • x + b • y) ≤ a • g x + b • g y := hg.right hx hy ha hb hab
_ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_right
