Local Geometry Step 2: Fiber Integration for Quadratic Growth and Strong Aiming

Fix x ∈ U₊, m = π(x), e = x - m. Define φ(t) = f(m + te). Since U₊ is fiber-saturated, m + te ∈ U₊ for t ∈ [0,1].

φ(0) = f⋆, φ'(0) = 0, φ''(t) = eᵀ D²f(m+te) e ≥ μ'‖e‖².

Quadratic growth (integrate φ'' twice):

f(x) - f⋆ = φ(1) - φ(0) = ∫₀¹ (1-t) φ''(t) dt ≥ (μ'/2)‖e‖²

Strong aiming (integration by parts):

⟨∇f(x), e⟩ - (f(x) - f⋆) = φ'(1) - (φ(1) - φ(0)) = ∫₀¹ t φ''(t) dt ≥ (μ'/2)‖e‖² So ⟨∇f(x), e⟩ ≥ f(x) - f⋆ + (μ'/2)‖e‖²

theorem PLAcceleratedNesterovLean.differentiable_deriv_of_contDiff2 {φ : ℝ → ℝ} (hφ : ContDiff ℝ 2 φ) : Differentiable ℝ (deriv φ)

theorem PLAcceleratedNesterovLean.hasDerivAt_const_mul_id (c x : ℝ) : HasDerivAt (fun (t : ℝ) => c * t) c x

theorem PLAcceleratedNesterovLean.hasDerivAt_quad (c x : ℝ) : HasDerivAt (fun (t : ℝ) => c / 2 * t ^ 2) (c * x) x

theorem PLAcceleratedNesterovLean.differentiable_sq : Differentiable ℝ fun (t : ℝ) => t ^ 2

theorem PLAcceleratedNesterovLean.continuous_sq : Continuous fun (t : ℝ) => t ^ 2

theorem PLAcceleratedNesterovLean.quadratic_growth_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φ'_zero : deriv φ 0 = 0) (hφ''_lower : ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → deriv (deriv φ) t ≥ c) : φ 1 - φ 0 ≥ c / 2

If φ''(t) ≥ c for all t ∈ [0,1] and φ'(0) = 0, then φ(1) - φ(0) ≥ c/2. (Quadratic growth from Hessian lower bound.) Localized version: only requires ContinuousOn/DifferentiableOn on [0,1].

theorem PLAcceleratedNesterovLean.strong_aiming_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φ'_zero : deriv φ 0 = 0) (hφ''_lower : ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → deriv (deriv φ) t ≥ c) : deriv φ 1 ≥ φ 1 - φ 0 + c / 2

If φ''(t) ≥ c for all t ∈ [0,1] and φ'(0) = 0, then φ'(1) ≥ φ(1) - φ(0) + c/2. (Strong aiming from integration by parts.) Localized version: only requires ContinuousOn/DifferentiableOn on [0,1].

theorem PLAcceleratedNesterovLean.fiber_deriv {d : ℕ} (f : E d → ℝ) (m e : E d) (hf : Differentiable ℝ f) (t : ℝ) : deriv (fun (s : ℝ) => f (m + s • e)) t = inner ℝ (gradient f (m + t • e)) e

The fiber function φ(t) = f(m + t·e) has φ'(t) = ⟨∇f(m+te), e⟩.