Differentiating Convex Functions Constructively

Hannes Diener and Matthew Hendtlass

In the paper 'Differentiating Convex Functions Constructively' by Hannes Diener and Matthew Hendtlass, the increase in 'the approximate derivatives of f ' for convex functions f : [0, 1] → ℝ is proved in Lemma 3. Here we formalize the proof.

Note that the proof provided in the paper does not account for the case when y = x'. Because of this (and for effieciency) the proof was changed, but we attempt to keep the spirit of the proof.

Also note that the formalization uses f : ℝ → ℝ instead of f : ↑(Set.Icc 0 1) → ℝ because the ConvexOn in Mathlib would require that 'AddCommMonoid ↑(Set.Icc 0 1)'.

theorem abcdef (a b c d e f : ℝ) : c ≤ a - b + d + e - f → f ≤ a - b - c + d + e

theorem Neighbors {x z y : ℝ} (f : ℝ → ℝ) (Con : ConvexOn ℝ (Set.Icc 0 1) f) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) (ha1 : x < y) (ha2 : y < z) : (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

theorem Lemma_3 {x y x' y' : ℝ} (f : ℝ → ℝ) (Con : ConvexOn ℝ (Set.Icc 0 1) f) (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc 0 1) (hx' : x' ∈ Set.Icc 0 1) (hy' : y' ∈ Set.Icc 0 1) (ha1 : x < y) (ha2 : y ≤ x') (ha3 : x' < y') : (f y - f x) / (y - x) ≤ (f y' - f x') / (y' - x')