Comparing right derivatives of convex functions

For real convex functions on an open interval, inequalities between slopes on adjacent intervals imply inequalities between their right derivatives. If the slopes interlace in both directions, the difference of the functions is constant on the interval. These results support uniqueness up to an additive constant when derivatives agree only on a dense set.

Main statements

• TauCeti.rightDeriv_le_of_slope_le compares right derivatives from adjacent-slope inequalities.
• TauCeti.sub_eq_sub_of_slope_le proves constancy of the difference when the slopes interlace.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, §24 (one-sided derivatives of convex functions).

theorem TauCeti.rightDeriv_le_of_slope_le {φ ψ : ℝ → ℝ} {I : Set ℝ} (hI : IsOpen I) (hφ : ConvexOn ℝ I φ) (hψ : ConvexOn ℝ I ψ) (h : ∀ (a b c : ℝ), a ∈ I → c ∈ I → a < b → b < c → slope φ a b ≤ slope ψ b c) {b : ℝ} (hb : b ∈ I) : derivWithin φ (Set.Ioi b) b ≤ derivWithin ψ (Set.Ioi b) b

If no slope of φ on an interval [a, b] exceeds a slope of ψ on an adjacent interval [b, c], then the right derivative of φ is at most that of ψ.

theorem TauCeti.sub_eq_sub_of_slope_le {φ ψ : ℝ → ℝ} {I : Set ℝ} (hI : IsOpen I) (hφ : ConvexOn ℝ I φ) (hψ : ConvexOn ℝ I ψ) (h₁ : ∀ (a b c : ℝ), a ∈ I → c ∈ I → a < b → b < c → slope φ a b ≤ slope ψ b c) (h₂ : ∀ (a b c : ℝ), a ∈ I → c ∈ I → a < b → b < c → slope ψ a b ≤ slope φ b c) {s t : ℝ} (hs : s ∈ I) (ht : t ∈ I) (hst : s ≤ t) : φ t - ψ t = φ s - ψ s

Two convex functions on an open interval whose slopes interlace in both directions differ by a constant.