Internal Assembly for the Main Theorem

This file contains helper statements used by PLAcceleratedNesterovLean.MainTheorem. The public file intentionally exposes only the clean top-level theorem.

Shared packaging helpers

Main theorem: state positions, prefactor 2

theorem PLAcceleratedNesterovLean.nesterov_pl_accelerated_rate_theta {d : ℕ} (hd : 0 < d) (L : NNReal) (hL : 0 < ↑L) (μ : ℝ) (hμ : 0 < μ) (θ : ℝ) (hθ_pos : 0 < θ) (hθ_le : θ ≤ √(μ / ↑L) / 8) (f : E d → ℝ) (n : ℕ) (M : Type u_1) [TopologicalSpace M] [ChartedSpace (ManifoldModel n) M] [IsManifold (modelI n) 2 M] [Nonempty M] (ι : M → E d) : Manifold.IsSmoothEmbedding (modelI n) (modelWithCornersSelf ℝ (E d)) 2 ι → Set.range ι = argminSet f → ∀ (U : Set (E d)), IsGeneralTubularNeighborhood (Set.range ι) U → ContDiffOn ℝ 2 f U → PolyakLojasiewicz f μ U → LipschitzOnWith L (gradient f) U → ∃ (Ū : Set (E d)), IsOpen Ū ∧ Set.range ι ⊆ Ū ∧ Ū ⊆ U ∧ ∀ x₀ ∈ Ū, (∀ (k : ℕ), (nesterovSeqGen f (1 / ↑L) (rhoOfTheta (↑L) μ θ) { x := x₀, v := 0 } k).x ∈ U ∧ (nesterovSeqGen f (1 / ↑L) (rhoOfTheta (↑L) μ θ) { x := x₀, v := 0 } k).lookahead (1 / ↑L) ∈ U) ∧ HasAcceleratedRateWithPrefactorTwo f (fun (k : ℕ) => (nesterovSeqGen f (1 / ↑L) (rhoOfTheta (↑L) μ θ) { x := x₀, v := 0 } k).x) (↑L) μ x₀ ∧ HasAcceleratedRate f (fun (k : ℕ) => (nesterovSeqGen f (1 / ↑L) (rhoOfTheta (↑L) μ θ) { x := x₀, v := 0 } k).x) (↑L) μ

Explicit-θ form of the main theorem.

Fix a retuning parameter θ satisfying 0 < θ ≤ √(μ/L)/8. When the standard compatibility bound μ ≤ L holds, the proof delegates to the local convergence theorem. In the complementary L < μ case, any local non-minimizer would force μ ≤ L, so the theorem is discharged by the stationary local-constant branch.

For every objective whose minimizer set is an embedded submanifold and which satisfies the local PL, smoothness, and tubular-neighborhood hypotheses, there is an open neighborhood of the minimizer manifold such that Nesterov's state positions stay in the original tubular neighborhood and satisfy

f(xₖ) - f⋆ ≤ 2 * exp(-k / sqrt (L / μ)) * (f(x₀) - f⋆).

theorem PLAcceleratedNesterovLean.nesterov_pl_accelerated_rate_embedded {d : ℕ} (L : NNReal) (μ : ℝ) : ∃ (ρ : ℝ), ∀ (f : E d → ℝ) (n : ℕ) (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : ChartedSpace (ManifoldModel n) M] [IsManifold (modelI n) 2 M] [Nonempty M] (ι : M → E d), Manifold.IsSmoothEmbedding (modelI n) (modelWithCornersSelf ℝ (E d)) 2 ι → Set.range ι = argminSet f → ∀ (U : Set (E d)), IsOpen U → Set.range ι ⊆ U → ContDiffOn ℝ 2 f U → PolyakLojasiewicz f μ U → LipschitzOnWith L (gradient f) U → ∃ (Ū : Set (E d)), IsOpen Ū ∧ Set.range ι ⊆ Ū ∧ Ū ⊆ U ∧ ∀ x₀ ∈ Ū, ∀ (k : ℕ), (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } k).x ∈ U ∧ (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } k).lookahead (1 / ↑L) ∈ U ∧ f (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } k).x - fStar f ≤ 2 * Real.exp (-(↑k / √(↑L / μ))) * (f x₀ - fStar f)

Main theorem (public form).

There exists a momentum parameter ρ, depending only on L and μ, such that for every objective whose minimizer set is an embedded submanifold and which satisfies the local PL and smoothness hypotheses on an open neighborhood of the minimizer manifold, there is a smaller open neighborhood such that Nesterov's state positions stay in the original neighborhood and satisfy the explicit prefactor-two estimate

f(xₖ) - f⋆ ≤ 2 * exp(-k / sqrt (L / μ)) * (f(x₀) - f⋆).

This internal form exposes the embedded-manifold witness directly; the public theorem in PLAcceleratedNesterovLean.MainTheorem re-exports exactly these report-level assumptions from a clean file.

theorem PLAcceleratedNesterovLean.nesterov_pl_accelerated_rate_c3_internal {d : ℕ} (L : NNReal) (μ : ℝ) : ∃ (ρ : ℝ), ∀ (f : E d → ℝ) (U : Set (E d)), IsOpen U → argminSet f ⊆ U → ContDiffOn ℝ 3 f U → PolyakLojasiewicz f μ U → LipschitzOnWith L (gradient f) U → ∃ (Ū : Set (E d)), IsOpen Ū ∧ argminSet f ⊆ Ū ∧ Ū ⊆ U ∧ ∀ x₀ ∈ Ū, ∀ (k : ℕ), (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } k).x ∈ U ∧ (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } k).lookahead (1 / ↑L) ∈ U ∧ f (nesterovSeqGen f (1 / ↑L) ρ { x := x₀, v := 0 } k).x - fStar f ≤ 2 * Real.exp (-(↑k / √(↑L / μ))) * (f x₀ - fStar f)

C³-only internal main theorem.

This variant assumes f is C³ on an open neighborhood of its global minimizer set. The C³+PL Morse-Bott machinery constructs the tubular sub-neighborhood internally from the first-order theorem hypotheses.