Motion Error Step 1: Gradient Bound from L-Smoothness

Since π(x'_n) ∈ M and ∇f(π(x'_n)) = 0, L-smoothness gives: ‖g_n‖ = ‖∇f(x'_n) - ∇f(π(x'_n))‖ ≤ L · ‖x'_n - π(x'_n)‖ = L · ‖e_n‖

Combined with ‖e_n‖² ≤ C_coer/μ' · L_n from coercivity: ‖g_n‖ ≤ L · √(C_coer/μ') · √L_n =: C_g · √L_n

theorem PLAcceleratedNesterovLean.gradient_bound_from_lipschitz {d : ℕ} (f : E d → ℝ) (L : NNReal) {V : Set (E d)} (hf_lip : LipschitzOnWith L (gradient f) V) (x y : E d) (hx_V : x ∈ V) (hy_V : y ∈ V) (hzero : gradient f y = 0) : ‖gradient f x‖ ≤ ↑L * ‖x - y‖

If gradient is L-Lipschitz on V and ∇f(y) = 0, then ‖∇f(x)‖ ≤ L·‖x - y‖.

theorem PLAcceleratedNesterovLean.velocity_bound_from_step {d : ℕ} (v g : E d) (ρ sqrtη : ℝ) : ‖ρ • (v - sqrtη • g)‖ ≤ |ρ| * (‖v‖ + |sqrtη| * ‖g‖)

Velocity bound: ‖v_{n+1}‖ = ‖ρ(v_n - √η g_n)‖ ≤ |ρ|(‖v_n‖ + √η ‖g_n‖).

theorem PLAcceleratedNesterovLean.step_bound {d : ℕ} (v_next g : E d) (sqrtη η : ℝ) : ‖sqrtη • v_next - η • g‖ ≤ |sqrtη| * ‖v_next‖ + |η| * ‖g‖

Step bound: h_n = √η v_{n+1} - η g_n, so ‖h_n‖ ≤ √η‖v_{n+1}‖ + η‖g_n‖.