Smooth segment estimates

Adapted from CoarseGraining (LeanIntoHomogenization, 2026) with the author's permission. These are the smooth one-dimensional estimates used by the unit-ball Poincare proof.

theorem CKN.sub_eq_integral_fderiv_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ 1 u) (x y : Vec d) : u x - u y = ∫ (t : ℝ) in 0..1, (fderiv ℝ u (segmentBlend x t y)) (x - y)

theorem CKN.norm_sub_le_integral_fderiv_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ 1 u) (x y : Vec d) : ‖u x - u y‖ ≤ ∫ (t : ℝ) in 0..1, ‖(fderiv ℝ u (segmentBlend x t y)) (x - y)‖

theorem CKN.norm_sub_le_integral_norm_fderiv_mul_norm_sub_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ 1 u) (x y : Vec d) : ‖u x - u y‖ ≤ ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖