Gluing convex functions at a point

A real function which is convex on (-∞, a] and on [a, ∞) is convex on all of ℝ as soon as its left derivative at a is at most its right derivative there. This is the standard way to prove convexity of a function given by different formulas on the two sides of a point, for instance a function of |x|, and complements the monotone and antitone gluing lemmas of Mathlib.Analysis.Convex.Piecewise.

Main statements

• TauCeti.convexOn_univ_of_convexOn_Iic_Ici: a function convex on both sides of a whose one-sided derivatives at a satisfy f'(a⁻) ≤ f'(a⁺) is convex on ℝ.

theorem TauCeti.convexOn_univ_of_convexOn_Iic_Ici {f : ℝ → ℝ} {a m₁ m₂ : ℝ} (hl : ConvexOn ℝ (Set.Iic a) f) (hr : ConvexOn ℝ (Set.Ici a) f) (hl' : HasDerivWithinAt f m₁ (Set.Iic a) a) (hr' : HasDerivWithinAt f m₂ (Set.Ici a) a) (hm : m₁ ≤ m₂) : ConvexOn ℝ Set.univ f

Gluing convex functions: if f : ℝ → ℝ is convex on (-∞, a] and on [a, ∞), and its derivative m₁ at a within (-∞, a] is at most its derivative m₂ at a within [a, ∞), then f is convex on ℝ.