theorem helperForProposition_6_13_2_uniformDerivWithinNormUpperBound {a b : ℝ} (f : ℝ → ℝ) (hcontDeriv : ContinuousOn (derivWithin f (Set.Icc a b)) (Set.Icc a b)) (hderiv_lt_one : ∀ x ∈ Set.Icc a b, |derivWithin f (Set.Icc a b) x| < 1) : ∃ c0 < 1, ∀ x ∈ Set.Icc a b, ‖derivWithin f (Set.Icc a b) x‖ ≤ c0

Helper for Proposition 6.13(2): continuity of derivWithin and the pointwise bound |derivWithin| < 1 on Icc a b imply a uniform constant c0 < 1 with ‖derivWithin f (Icc a b) x‖ ≤ c0 on Icc a b.

theorem helperForProposition_6_13_2_positiveContractionConstant {a b : ℝ} (f : ℝ → ℝ) {c0 : ℝ} (hc0_lt_one : c0 < 1) (hbound : ∀ x ∈ Set.Icc a b, ‖derivWithin f (Set.Icc a b) x‖ ≤ c0) : ∃ (c : ℝ), 0 < c ∧ c < 1 ∧ ∀ x ∈ Set.Icc a b, ‖derivWithin f (Set.Icc a b) x‖ ≤ c

Helper for Proposition 6.13(2): from a strict upper bound c0 < 1 on ‖derivWithin f (Icc a b) x‖, build a positive contraction constant c ∈ (0,1).

theorem helperForProposition_6_13_2_absDifferenceBoundFromDerivWithinBound {a b : ℝ} (f : ℝ → ℝ) (hdiff : DifferentiableOn ℝ f (Set.Icc a b)) {c : ℝ} (hderiv_le : ∀ z ∈ Set.Icc a b, ‖derivWithin f (Set.Icc a b) z‖ ≤ c) (x : ℝ) : x ∈ Set.Icc a b → ∀ y ∈ Set.Icc a b, |f x - f y| ≤ c * |x - y|

Helper for Proposition 6.13(2): a uniform bound on ‖derivWithin f (Icc a b) x‖ implies the Lipschitz estimate |f x - f y| ≤ c * |x - y| on Icc a b.

theorem deriv_strict_bound_on_interval_implies_strict_contraction {a b : ℝ} (f : ℝ → ℝ) (_hmaps : Set.MapsTo f (Set.Icc a b) (Set.Icc a b)) (hdiff : DifferentiableOn ℝ f (Set.Icc a b)) (hcontDeriv : ContinuousOn (derivWithin f (Set.Icc a b)) (Set.Icc a b)) (hderiv_lt_one : ∀ x ∈ Set.Icc a b, |derivWithin f (Set.Icc a b) x| < 1) : ∃ (c : ℝ), 0 < c ∧ c < 1 ∧ ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ c * |x - y|

Proposition 6.13(2): if f : [a,b] → [a,b] is differentiable, f' is continuous on [a,b], and |f'(x)| < 1 for all x ∈ [a,b], then there exists c ∈ (0,1) such that |f(x) - f(y)| ≤ c * |x - y| for all x,y ∈ [a,b]. In particular, the induced self-map of [a,b] is a strict contraction for the metric d(x,y) = |x - y|.