Convex and concave piecewise functions

This file proves convex and concave theorems for piecewise functions.

Main statements

• convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici is the proof that the piecewise function (Set.Iic e).piecewise f g of a function f decreasing and convex on Set.Iic e and a function g increasing and convex on Set.Ici e, such that f e = g e, is convex on the universal set.

  This version has the boundary point included in the left-hand function.

  See convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic for the version with the boundary point included in the right-hand function.

  See concave version(s) concaveOn_univ_piecewise_Iic_of_monotoneOn_Iic_antitoneOn_Ici and concaveOn_univ_piecewise_Ici_of_antitoneOn_Ici_monotoneOn_Iic.

theorem convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] [OrderedAddCommGroup β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β} (hf : ConvexOn 𝕜 (Set.Iic e) f) (hg : ConvexOn 𝕜 (Set.Ici e) g) (h_anti : AntitoneOn f (Set.Iic e)) (h_mono : MonotoneOn g (Set.Ici e)) (h_eq : f e = g e) : ConvexOn 𝕜 Set.univ ((Set.Iic e).piecewise f g)

The piecewise function (Set.Iic e).piecewise f g of a function f decreasing and convex on Set.Iic e and a function g increasing and convex on Set.Ici e, such that f e = g e, is convex on the universal set.

theorem convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] [OrderedAddCommGroup β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β} (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)

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 concaveOn_univ_piecewise_Iic_of_monotoneOn_Iic_antitoneOn_Ici {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] [OrderedAddCommGroup β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β} (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)

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_Ici_of_antitoneOn_Ici_monotoneOn_Iic {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] [OrderedAddCommGroup β] [Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β} (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)

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.