English
Let f and g be strictly convex on a common domain s. Then their pointwise maximum h(x) = max{f(x), g(x)} is also strictly convex on s.
Русский
Пусть f и g строго выпуклы на одной области s. Тогда их точечное максимумы h(x) = max{f(x), g(x)} также строго выпукла на s.
LaTeX
$$$\StrictConvexOn(\mathfrak{K}, s, f) \\land \\StrictConvexOn(\mathfrak{K}, s, g) \Rightarrow \StrictConvexOn(\mathfrak{K}, s, x \mapsto \max\{f(x), g(x)\})$$$
Lean4
/-- The pointwise maximum of strictly convex functions is strictly convex. -/
theorem sup (hf : StrictConvexOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) : StrictConvexOn 𝕜 s (f ⊔ g) :=
⟨hf.left, fun x hx y hy hxy a b ha hb hab =>
max_lt
(calc
f (a • x + b • y) < a • f x + b • f y := hf.2 hx hy hxy 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.2 hx hy hxy ha hb hab
_ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_right)⟩
