English
The piecewise function on Iic e and Iic e with f decreasing and convex, g increasing and convex, and f(e)=g(e), is convex on all of R.
Русский
Пошаговая функция на Iic e и Iic e, где f убывающая и выпуклая, g возрастающая и выпуклая, и f(e)=g(e), выпукла на всей прямой.
LaTeX
$$$ ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise f g) $$$
Lean4
/-- The piecewise function `(Set.Ici e).piecewise f g` of a function `f` increasing and convex on
`Set.Ici e` and a function `g` decreasing and convex on `Set.Iic e`, such that `f e = g e`, is
convex on the universal set. -/
theorem convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic (hf : ConvexOn 𝕜 (Set.Ici e) f)
(hg : ConvexOn 𝕜 (Set.Iic e) g) (h_mono : MonotoneOn f (Set.Ici e)) (h_anti : AntitoneOn g (Set.Iic e))
(h_eq : f e = g e) : ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise f g) :=
by
have h_piecewise_Ici_eq_piecewise_Iic : (Set.Ici e).piecewise f g = (Set.Iic e).piecewise g f := by ext x;
by_cases hx : x = e <;> simp [Set.piecewise, @le_iff_lt_or_eq _ _ x e, ← @ite_not _ (e ≤ _), hx, h_eq]
rw [h_piecewise_Ici_eq_piecewise_Iic]
exact convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici hg hf h_anti h_mono h_eq.symm
