Modified Nesterov Scheme and Supporting Definitions

Shared definitions for the proof of local accelerated convergence:

• Modified Nesterov iteration (state, step, sequence)
• Hessian quadratic form
• Lyapunov function and auxiliary quantities
• Fiber-saturated sets
• Tangent/normal space of an embedded manifold

Hessian quadratic form

noncomputable def PLAcceleratedNesterovLean.hessianQuadForm {d : ℕ} (f : E d → ℝ) (x ξ : E d) : ℝ

The Hessian quadratic form: ξᵀ D²f(x) ξ = ⟨(D(∇f)(x)) ξ, ξ⟩.

Equations

• PLAcceleratedNesterovLean.hessianQuadForm f x ξ = inner ℝ ((fderiv ℝ (gradient f) x) ξ) ξ

Modified Nesterov scheme

structure PLAcceleratedNesterovLean.NesterovState (d : ℕ) : Type

State of the modified Nesterov scheme: position x and velocity v.

• x : E d

  The current position.

• v : E d

  The current velocity.

noncomputable def PLAcceleratedNesterovLean.NesterovState.lookahead {d : ℕ} (s : NesterovState d) (η : ℝ) : E d

The look-ahead point x' = x + √η · v.

Equations

• s.lookahead η = s.x + √η • s.v

noncomputable def PLAcceleratedNesterovLean.nesterovStep {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (s : NesterovState d) : NesterovState d

One step of the modified Nesterov scheme: x' = x + √η · v (look-ahead) g = ∇f(x') (gradient at look-ahead) x₊ = x' - η · g (gradient step) v₊ = ρ(v - √η · g) (momentum update)

Equations

• PLAcceleratedNesterovLean.nesterovStep f η ρ s = { x := s.lookahead η - η • gradient f (s.lookahead η), v := ρ • (s.v - √η • gradient f (s.lookahead η)) }

def PLAcceleratedNesterovLean.nesterovSeq {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) : ℕ → NesterovState d

The Nesterov sequence starting from x₁ with v₁ = 0. Index 0 corresponds to iteration 1 in the paper.

Equations

• PLAcceleratedNesterovLean.nesterovSeq f η ρ x₁ 0 = { x := x₁, v := 0 }
• PLAcceleratedNesterovLean.nesterovSeq f η ρ x₁ n.succ = PLAcceleratedNesterovLean.nesterovStep f η ρ (PLAcceleratedNesterovLean.nesterovSeq f η ρ x₁ n)

noncomputable def PLAcceleratedNesterovLean.nesterovGrad {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : E d

The gradient computed at the look-ahead point at step n.

Equations

• PLAcceleratedNesterovLean.nesterovGrad f η ρ x₁ n = gradient f ((PLAcceleratedNesterovLean.nesterovSeq f η ρ x₁ n).lookahead η)

noncomputable def PLAcceleratedNesterovLean.nesterovH {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : E d

Step between consecutive look-ahead points: h_n = x'_{n+1} - x'_n.

Equations

• PLAcceleratedNesterovLean.nesterovH f η ρ x₁ n = (PLAcceleratedNesterovLean.nesterovSeq f η ρ x₁ (n + 1)).lookahead η - (PLAcceleratedNesterovLean.nesterovSeq f η ρ x₁ n).lookahead η

Geometric quantities

noncomputable def PLAcceleratedNesterovLean.normalDisp {d : ℕ} (π : E d → E d) (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : E d

Normal displacement: e_n = x'_n - π(x'_n), the error from the manifold. Here π is the nearest-point projection.

Equations

• PLAcceleratedNesterovLean.normalDisp π f η ρ x₁ n = (PLAcceleratedNesterovLean.nesterovSeq f η ρ x₁ n).lookahead η - π ((PLAcceleratedNesterovLean.nesterovSeq f η ρ x₁ n).lookahead η)

noncomputable def PLAcceleratedNesterovLean.auxVar {d : ℕ} (P : E d →L[ℝ] E d) (μ' : ℝ) (π : E d → E d) (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : E d

Auxiliary variable: u_n = P⊥ v_n + √μ' · e_n, where P⊥ = Id - P is the normal projector (P projects onto tangent space).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PLAcceleratedNesterovLean.curvatureError {d : ℕ} (P π : E d → E d) (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : E d

Curvature error: ξ_n = e_{n+1} - e_n - P⊥ h_n. Measures the deviation from the affine-case recursion.

Equations

• One or more equations did not get rendered due to their size.

Potential and Lyapunov functions

noncomputable def PLAcceleratedNesterovLean.psi {d : ℕ} (f : E d → ℝ) (μ' : ℝ) (S : Set (E d)) (x : E d) : ℝ

The potential Ψ(x) = f(x) - f⋆ + (μ'/2) · dist(x, S)². Combines the optimality gap with a quadratic distance penalty.

Equations

• PLAcceleratedNesterovLean.psi f μ' S x = f x - PLAcceleratedNesterovLean.fStar f + μ' / 2 * Metric.infDist x S ^ 2

noncomputable def PLAcceleratedNesterovLean.lyapunov {d : ℕ} (P : E d →L[ℝ] E d) (μ' : ℝ) (π : E d → E d) (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : ℝ

The Lyapunov function: L_n = (f(x_n) - f⋆) + ½‖u_n‖² + lam‖P v_n‖² where lam = (1+a)²/(2(1-a)) and a = √(μ'·η).

Equations

• One or more equations did not get rendered due to their size.

Fiber saturation

def PLAcceleratedNesterovLean.IsFiberSaturated {d : ℕ} (π : E d → E d) (A : Set (E d)) : Prop

A set A is fiber-saturated with respect to a projection π if for every x ∈ A, the segment from π(x) to x lies entirely in A.

Equations

• PLAcceleratedNesterovLean.IsFiberSaturated π A = ∀ x ∈ A, ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → (1 - t) • π x + t • x ∈ A

Tangent space of an embedded manifold

noncomputable def PLAcceleratedNesterovLean.tangentSubspace {d : ℕ} {M : Type u_1} {n : ℕ} (ι : M → E d) [TopologicalSpace M] [ChartedSpace (ManifoldModel n) M] (m : M) : Submodule ℝ (E d)

The tangent subspace of the embedded manifold at a point m, defined as the range of the manifold derivative of ι at m.

Equations

• PLAcceleratedNesterovLean.tangentSubspace ι m = (↑(mfderiv% ι m)).range