Generalized Nesterov Sequence and State-Based Definitions

Extends the Nesterov scheme with:

• nesterovSeqGen: sequence with arbitrary initial state (not just v=0)
• State-based Lyapunov, auxVar, and related definitions
• Equivalence with the original nesterovSeq definitions

These are needed for the Nesterov algorithm with arbitrary initial state (nonzero velocity).

Generalized Nesterov sequence

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

Generalized Nesterov sequence starting from an arbitrary initial state s₀. Generalization of nesterovSeq supporting nonzero initial velocity.

Equations

• PLAcceleratedNesterovLean.nesterovSeqGen f η ρ s₀ 0 = s₀
• PLAcceleratedNesterovLean.nesterovSeqGen f η ρ s₀ n.succ = PLAcceleratedNesterovLean.nesterovStep f η ρ (PLAcceleratedNesterovLean.nesterovSeqGen f η ρ s₀ n)

theorem PLAcceleratedNesterovLean.nesterovSeqGen_zero_vel {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : nesterovSeqGen f η ρ { x := x₁, v := 0 } n = nesterovSeq f η ρ x₁ n

nesterovSeq is nesterovSeqGen with zero initial velocity.

theorem PLAcceleratedNesterovLean.nesterovSeqGen_succ {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (s₀ : NesterovState d) (n : ℕ) : nesterovSeqGen f η ρ s₀ (n + 1) = nesterovStep f η ρ (nesterovSeqGen f η ρ s₀ n)

State-based auxiliary definitions

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

Normal displacement for a given state: e = x' − π(x').

Equations

• PLAcceleratedNesterovLean.normalDispOfState π η s = s.lookahead η - π (s.lookahead η)

noncomputable def PLAcceleratedNesterovLean.auxVarOfState {d : ℕ} (P : E d →L[ℝ] E d) (μ' : ℝ) (π : E d → E d) (η : ℝ) (s : NesterovState d) : E d

Auxiliary variable for a given state: u = P⊥v + √μ'·e.

Equations

• PLAcceleratedNesterovLean.auxVarOfState P μ' π η s = s.v - P s.v + √μ' • PLAcceleratedNesterovLean.normalDispOfState π η s

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

Curvature error for a step: ξ = e' − e − P⊥h.

Equations

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

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

Step displacement h = x'_{n+1} − x'_n for a given state.

Equations

• PLAcceleratedNesterovLean.stepDispOfState f η ρ s = (PLAcceleratedNesterovLean.nesterovStep f η ρ s).lookahead η - s.lookahead η

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

Gradient at the lookahead point for a given state.

Equations

• PLAcceleratedNesterovLean.gradOfState f η s = gradient f (s.lookahead η)

noncomputable def PLAcceleratedNesterovLean.lyapunovOfState {d : ℕ} (P : E d →L[ℝ] E d) (μ' : ℝ) (π : E d → E d) (f : E d → ℝ) (η : ℝ) (s : NesterovState d) : ℝ

State-based Lyapunov function: L(s) = (f(x) − f⋆) + ½‖u‖² + λ‖Pv‖² where u = P⊥v + √μ'·e, λ = (1+a)²/(2(1−a)), a = √(μ'·η).

Equations

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

Equivalence with nesterovSeq-based definitions

theorem PLAcceleratedNesterovLean.normalDispOfState_eq_normalDisp {d : ℕ} (π : E d → E d) (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : normalDispOfState π η (nesterovSeq f η ρ x₁ n) = normalDisp π f η ρ x₁ n

theorem PLAcceleratedNesterovLean.auxVarOfState_eq_auxVar {d : ℕ} (P : E d →L[ℝ] E d) (μ' : ℝ) (π : E d → E d) (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : auxVarOfState P μ' π η (nesterovSeq f η ρ x₁ n) = auxVar P μ' π f η ρ x₁ n

theorem PLAcceleratedNesterovLean.stepDispOfState_eq_nesterovH {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : stepDispOfState f η ρ (nesterovSeq f η ρ x₁ n) = nesterovH f η ρ x₁ n

theorem PLAcceleratedNesterovLean.gradOfState_eq_nesterovGrad {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : gradOfState f η (nesterovSeq f η ρ x₁ n) = nesterovGrad f η ρ x₁ n

theorem PLAcceleratedNesterovLean.curvatureErrorOfState_eq_curvatureError {d : ℕ} (P π : E d → E d) (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : curvatureErrorOfState P π f η ρ (nesterovSeq f η ρ x₁ n) = curvatureError P π f η ρ x₁ n

theorem PLAcceleratedNesterovLean.lyapunovOfState_eq_lyapunov {d : ℕ} (P : E d →L[ℝ] E d) (μ' : ℝ) (π : E d → E d) (f : E d → ℝ) (η ρ : ℝ) (x₁ : E d) (n : ℕ) : lyapunovOfState P μ' π f η (nesterovSeq f η ρ x₁ n) = lyapunov P μ' π f η ρ x₁ n

Basic properties

theorem PLAcceleratedNesterovLean.lyapunovOfState_nonneg {d : ℕ} (P : E d →L[ℝ] E d) (μ' : ℝ) (π : E d → E d) (f : E d → ℝ) (η : ℝ) (s : NesterovState d) (hμ' : 0 < μ') (hη : 0 < η) (hμη : μ' * η < 1) (hbdd : BddBelow (Set.range f)) : 0 ≤ lyapunovOfState P μ' π f η s