Bootstrap Step 1: Geometric Decay by Induction

If Lₙ₊₁ ≤ c · Lₙ whenever a predicate P(n) holds, and P is preserved, then Lₙ ≤ cⁿ · L₀.

Geometric Series Sum

S_a = Σ_{k=0}^∞ (1-a/2)^{k/2} = 1/(1-√(1-a/2)) is finite for a > 0.

Total Displacement Control

Σ_{k=1}^n ‖h_k‖ ≤ C_h √η Σ_{k=1}^n √L_k ≤ C_h √η · R · S_a

theorem PLAcceleratedNesterovLean.geometric_decay (f : ℕ → ℝ) (c : ℝ) (hc : 0 ≤ c) (hstep : ∀ (n : ℕ), f (n + 1) ≤ c * f n) (n : ℕ) : f n ≤ c ^ n * f 0

Geometric decay: if f(n+1) ≤ c * f(n) for all n, then f(n) ≤ c^n * f(0).

theorem PLAcceleratedNesterovLean.geometric_decay_with_invariant (f : ℕ → ℝ) (P : ℕ → Prop) (c : ℝ) (hc : 0 ≤ c) (_hc1 : c ≤ 1) (_hf0 : 0 ≤ f 0) (hP0 : P 0) (hstep : ∀ (n : ℕ), P n → f (n + 1) ≤ c * f n ∧ P (n + 1)) (n : ℕ) : P n ∧ f n ≤ c ^ n * f 0

Geometric decay with invariant: if contraction holds whenever P(n) is true, and P is preserved, then both the invariant and the decay hold for all n.

theorem PLAcceleratedNesterovLean.partial_geom_series_bound (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) (n : ℕ) : ∑ k ∈ Finset.range n, r ^ k ≤ 1 / (1 - r)

Partial geometric series: Σ_{k=0}^{n-1} r^k ≤ 1/(1-r) for 0 ≤ r < 1.

theorem PLAcceleratedNesterovLean.telescoping_norm_bound {d : ℕ} (x : ℕ → E d) (n : ℕ) : ‖x n - x 0‖ ≤ ∑ k ∈ Finset.range n, ‖x (k + 1) - x k‖

Telescoping sum: ‖x_{n+1} - x_1‖ ≤ Σ_{k=0}^{n-1} ‖x_{k+1} - x_k‖.