Auxiliary Variable Recursion for Lyapunov Contraction

The sequence-indexed recursion is the zero-velocity sequence specialization of the state-based one-step identity auxVarOfState_step.

theorem PLAcceleratedNesterovLean.auxVar_recursion {d : ℕ} (P : E d →L[ℝ] E d) (μ' η ρ : ℝ) (π : E d → E d) (f : E d → ℝ) (x₁ : E d) (n : ℕ) (hρ : ρ = (1 - √(μ' * η)) / (1 + √(μ' * η))) (ha_pos : 0 < √(μ' * η)) (hη_pos : 0 < η) (hμ_pos : 0 < μ') : have sn := nesterovSeq f η ρ x₁ n; have gn := gradient f (sn.lookahead η); have en := normalDisp π f η ρ x₁ n; have ξn := curvatureError (⇑P) π f η ρ x₁ n; have a := √(μ' * η); auxVar P μ' π f η ρ x₁ (n + 1) = (1 - a) • (sn.v - P sn.v) + √μ' • en - √η • (gn - P gn) + √μ' • ξn