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