The exact two-point, symmetric-in-|τ - τ'| Lipschitz bound that a uniform derivative bound on an interval gives — the abstract real-analysis fact behind the time-pairing estimate hpair in the corresponding statement (the pairing bound |g τ - g τ'| ≤ C |τ - τ'|).

theorem CIV.abs_sub_le_of_hasDerivWithinAt_le {g D : ℝ → ℝ} {a b C : ℝ} (hab : a ≤ b) (hC : 0 ≤ C) (hderiv : ∀ x ∈ Set.Icc a b, HasDerivWithinAt g (D x) (Set.Icc a b) x) (hbound : ∀ x ∈ Set.Ico a b, |D x| ≤ C) : |g b - g a| ≤ C * (b - a)

theorem CIV.abs_sub_le_of_hasDerivWithinAt_le_abs {g D : ℝ → ℝ} {a b C : ℝ} (hab : a ≤ b) (hC : 0 ≤ C) (hderiv : ∀ x ∈ Set.Icc a b, HasDerivWithinAt g (D x) (Set.Icc a b) x) (hbound : ∀ x ∈ Set.Ico a b, |D x| ≤ C) {τ τ' : ℝ} (hτ : τ ∈ Set.Icc a b) (hτ' : τ' ∈ Set.Icc a b) : |g τ - g τ'| ≤ C * |τ - τ'|

theorem CIV.abs_sub_le_of_forall_hasDerivAt_le {g D : ℝ → ℝ} {a b C : ℝ} (hab : a ≤ b) (hC : 0 ≤ C) (hderiv : ∀ (x : ℝ), HasDerivAt g (D x) x) (hbound : ∀ x ∈ Set.Icc a b, |D x| ≤ C) {τ τ' : ℝ} (hτ : τ ∈ Set.Icc a b) (hτ' : τ' ∈ Set.Icc a b) : |g τ - g τ'| ≤ C * |τ - τ'|