Definitions for Nesterov Acceleration under a Local Polyak-Łojasiewicz Condition

Core definitions: ambient space, optimization concepts (argmin, PL condition, L-smoothness), tubular neighborhoods, first-order algorithm model, convergence rate, and manifold setup.

@[reducible, inline]

abbrev PLAcceleratedNesterovLean.E (d : ℕ) : Type

The ambient Euclidean space ℝ^d.

Equations

• PLAcceleratedNesterovLean.E d = EuclideanSpace ℝ (Fin d)

Definitions for the optimization problem

def PLAcceleratedNesterovLean.argminSet {d : ℕ} (f : E d → ℝ) : Set (E d)

The set of global minimizers of f.

Equations

• PLAcceleratedNesterovLean.argminSet f = {x : PLAcceleratedNesterovLean.E d | ∀ (y : PLAcceleratedNesterovLean.E d), f x ≤ f y}

noncomputable def PLAcceleratedNesterovLean.fStar {d : ℕ} (f : E d → ℝ) : ℝ

The infimal value f⋆ = inf_x f(x).

Equations

• PLAcceleratedNesterovLean.fStar f = iInf f

def PLAcceleratedNesterovLean.PolyakLojasiewicz {d : ℕ} (f : E d → ℝ) (μ : ℝ) (U : Set (E d)) : Prop

A function f satisfies the μ-Polyak-Łojasiewicz (PL) condition on a set U if f is differentiable on U and ‖∇f(x)‖² ≥ 2μ(f(x) - f⋆) for all x ∈ U.

Equations

• PLAcceleratedNesterovLean.PolyakLojasiewicz f μ U = (0 < μ ∧ DifferentiableOn ℝ f U ∧ ∀ x ∈ U, ‖gradient f x‖ ^ 2 ≥ 2 * μ * (f x - PLAcceleratedNesterovLean.fStar f))

def PLAcceleratedNesterovLean.LSmooth {d : ℕ} (f : E d → ℝ) (L : NNReal) : Prop

L-smoothness: the gradient of f is L-Lipschitz.

Equations

• PLAcceleratedNesterovLean.LSmooth f L = (Differentiable ℝ f ∧ LipschitzWith L (gradient f))

structure PLAcceleratedNesterovLean.IsGeneralTubularNeighborhood {d : ℕ} (S U : Set (E d)) : Prop

U is a general tubular neighborhood of S: U is open, S ⊆ U, and every point in U has a unique nearest point in S.

• isOpen : IsOpen U
• subset : S ⊆ U
• uniqueProj (x : E d) : x ∈ U → ∃! p : E d, p ∈ S ∧ dist x p = Metric.infDist x S

First-order algorithm model

structure PLAcceleratedNesterovLean.FirstOrderAlgorithm (d : ℕ) : Type (u_1 + 1)

A first-order oracle algorithm with abstract internal state. At each step, the algorithm receives the function value f(x) and gradient ∇f(x) at the current readout point x, and produces a new internal state. The abstract state type S allows representing momentum methods like NAG (e.g. with S = E d × E d for the (xₖ, yₖ) pair).

• S : Type u_1

  The internal state type.

• init : E d → self.S

  Initialize the state from a starting point.

• step : self.S → ℝ → E d → self.S

  Advance one step: (state, f(readout(state)), ∇f(readout(state))) → new state.

• readout : self.S → E d

  Extract the current iterate from the internal state.

def PLAcceleratedNesterovLean.FirstOrderAlgorithm.stateAt {d : ℕ} (alg : FirstOrderAlgorithm d) (f : E d → ℝ) (x₀ : E d) : ℕ → alg.S

The sequence of internal states produced by a first-order algorithm.

Equations

• alg.stateAt f x₀ 0 = alg.init x₀
• alg.stateAt f x₀ k.succ = alg.step (alg.stateAt f x₀ k) (f (alg.readout (alg.stateAt f x₀ k))) (gradient f (alg.readout (alg.stateAt f x₀ k)))

noncomputable def PLAcceleratedNesterovLean.FirstOrderAlgorithm.iterate {d : ℕ} (alg : FirstOrderAlgorithm d) (f : E d → ℝ) (x₀ : E d) (k : ℕ) : E d

The sequence of iterates produced by a first-order algorithm.

Equations

• alg.iterate f x₀ k = alg.readout (alg.stateAt f x₀ k)

Convergence rate

def PLAcceleratedNesterovLean.HasAcceleratedRate {d : ℕ} (f : E d → ℝ) (iterates : ℕ → E d) (L μ : ℝ) : Prop

Accelerated convergence rate: f(xₖ) - f⋆ ≤ C · exp(-k / √(L/μ)).

Equations

• PLAcceleratedNesterovLean.HasAcceleratedRate f iterates L μ = ∃ (C : ℝ), 0 < C ∧ ∀ (k : ℕ), f (iterates k) - PLAcceleratedNesterovLean.fStar f ≤ C * Real.exp (-(↑k / √(L / μ)))

def PLAcceleratedNesterovLean.HasAcceleratedRateWithPrefactorTwo {d : ℕ} (f : E d → ℝ) (iterates : ℕ → E d) (L μ : ℝ) (x₀ : E d) : Prop

Accelerated convergence with explicit prefactor 2: f(xₖ) - f⋆ ≤ 2 · exp(-k / √(L/μ)) · (f(x₀) - f⋆).

Equations

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

Manifold setup: M as an embedded submanifold

@[reducible, inline]

abbrev PLAcceleratedNesterovLean.ManifoldModel (n : ℕ) : Type

The model space for the n-dimensional submanifold.

Equations

• PLAcceleratedNesterovLean.ManifoldModel n = EuclideanSpace ℝ (Fin n)

noncomputable def PLAcceleratedNesterovLean.modelI (n : ℕ) : ModelWithCorners ℝ (ManifoldModel n) (ManifoldModel n)

Model with corners for the n-dimensional Euclidean model (no boundary).

Equations

• PLAcceleratedNesterovLean.modelI n = modelWithCornersSelf ℝ (PLAcceleratedNesterovLean.ManifoldModel n)