English
The piecewise function on Ici e with f increasing and convex and g decreasing and convex, with f(e)=g(e), is convex on all of R.
Русский
Пошаговая функция на Ici e с f возрастанием и выпуклостью и g убыванием и выпуклостью, при f(e)=g(e), выпукла на всей прямой.
LaTeX
$$$ ConvexOn 𝕜 Set.univ ((Set.Ici e).piecewise f g) $$$
Lean4
/-- The piecewise function `(Set.Ici e).piecewise f g` of a function `f` decreasing and concave on
`Set.Ici e` and a function `g` increasing and concave on `Set.Iic e`, such that `f e = g e`, is
concave on the universal set. -/
theorem concaveOn_univ_piecewise_Ici_of_antitoneOn_Ici_monotoneOn_Iic (hf : ConcaveOn 𝕜 (Set.Ici e) f)
(hg : ConcaveOn 𝕜 (Set.Iic e) g) (h_anti : AntitoneOn f (Set.Ici e)) (h_mono : MonotoneOn g (Set.Iic e))
(h_eq : f e = g e) : ConcaveOn 𝕜 Set.univ ((Set.Ici e).piecewise f g) :=
by
rw [← neg_convexOn_iff, ← Set.piecewise_neg]
exact
convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic hf.neg hg.neg h_anti.neg h_mono.neg (neg_inj.mpr h_eq)
