Segment Estimate Helpers

Helper lemmas for the segment estimate used by motion_bounds_curvature_error. Provides a generalized strong aiming lemma (no φ'(0) = 0 requirement) and the fiber-path Hessian-to-second-derivative connection.

Generalized segment estimate

theorem PLAcceleratedNesterovLean.segment_estimate_from_hessian (φ : ℝ → ℝ) (c : ℝ) (hφ_cont : ContinuousOn φ (Set.Icc 0 1)) (hφ_diff : DifferentiableOn ℝ φ (Set.Ioo 0 1)) (hφ'_cont : ContinuousOn (deriv φ) (Set.Icc 0 1)) (hφ'_diff : DifferentiableOn ℝ (deriv φ) (Set.Ioo 0 1)) (hφ''_lower : ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → deriv (deriv φ) t ≥ c) : deriv φ 1 ≥ φ 1 - φ 0 + c / 2

General segment estimate: if φ is C² and φ''(t) ≥ c for t ∈ [0,1], then φ'(1) ≥ (φ(1) - φ(0)) + c/2.

Applies to C² functions with arbitrary φ'(0). The proof uses ψ(t) = t·φ'(t) - φ(t) + φ(0) - (c/2)t², which satisfies ψ(0) = 0 regardless of φ'(0) (since 0·φ'(0) = 0), and ψ'(t) = t·(φ''(t) - c) ≥ 0.

Fiber path second derivative = Hessian quadratic form

theorem PLAcceleratedNesterovLean.fiber_path_second_deriv {d : ℕ} (f : E d → ℝ) (m v : E d) (t : ℝ) (hf_C2 : ContDiffAt ℝ 2 f (m + t • v)) : deriv (deriv fun (s : ℝ) => f (m + s • v)) t = hessianQuadForm f (m + t • v) v

The second derivative of the fiber path φ(t) = f(m + t·v) equals the Hessian quadratic form at the corresponding point.

theorem PLAcceleratedNesterovLean.fiber_path_contDiff2 {d : ℕ} (f : E d → ℝ) (m v : E d) {V : Set (E d)} (hV : IsOpen V) (hf_C2 : ContDiffOn ℝ 2 f V) (hseg : ∀ (t : ℝ), m + t • v ∈ V) : ContDiff ℝ 2 fun (t : ℝ) => f (m + t • v)

The fiber path φ(t) = f(m + t·v) is C² when f is C² on an open set containing the entire line through m in direction v.

theorem PLAcceleratedNesterovLean.fiber_path_C2at_on_segment {d : ℕ} (f : E d → ℝ) (m v : E d) {V : Set (E d)} (hV : IsOpen V) (hf_C2 : ContDiffOn ℝ 2 f V) (hseg : ∀ t ∈ Set.Icc 0 1, m + t • v ∈ V) (t : ℝ) : t ∈ Set.Icc 0 1 → ContDiffAt ℝ 2 (fun (t : ℝ) => f (m + t • v)) t

The fiber path φ(t) = f(m + t·v) is C² at every point t ∈ [0,1] when f is C² on an open set containing the segment {m + t·v | t ∈ [0,1]}.