Multi-Phase Rate Arithmetic

Pure arithmetic lemmas for the multi-phase Nesterov convergence proof. These establish that:

1. The product ∏(1 + C·4⁻ᵏ) converges (finite jump overhead)
2. The geometric contraction (1-r)ⁿ ≤ exp(-n·r)
3. The total rate deficit Σ Nₖ·deficitₖ is bounded (summable)

All lemmas are independent of the Lean formalization of the algorithm.

Exponential bounds for geometric contraction

theorem PLAcceleratedNesterovLean.one_sub_pow_le_exp_neg {r : ℝ} (_hr0 : 0 ≤ r) (hr1 : r ≤ 1) (n : ℕ) : (1 - r) ^ n ≤ Real.exp (-(↑n * r))

(1 - r)^n ≤ exp(-n·r) for 0 ≤ r ≤ 1.

Product bounds for jump factors

theorem PLAcceleratedNesterovLean.prod_one_add_geometric_le {C r : ℝ} (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1) (K : ℕ) : ∏ k ∈ Finset.range K, (1 + C * r ^ (k + 1)) ≤ Real.exp (C * r / (1 - r))

Product of (1 + C·r^k) for k in range K is bounded by exp(C·r/(1-r)).

Rate deficit bounds

theorem PLAcceleratedNesterovLean.two_pow_mul_four_inv_pow (k : ℕ) : 2 ^ k * 4⁻¹ ^ k = (1 / 2) ^ k

2^k · 4^{-k} = (1/2)^k

theorem PLAcceleratedNesterovLean.rate_deficit_sum_le (K : ℕ) : ∑ k ∈ Finset.range K, 2 ^ k * 4⁻¹ ^ k ≤ 2

Σ_{k=0}^{K-1} 2^k · 4^{-k} = Σ (1/2)^k ≤ 2.

theorem PLAcceleratedNesterovLean.weighted_deficit_sum_le {C : ℝ} (hC : 0 ≤ C) (K : ℕ) : ∑ k ∈ Finset.range K, 2 ^ k * (C * 4⁻¹ ^ k) ≤ 2 * C

Σ_{k=0}^{K-1} 2^k · C · 4^{-k} ≤ 2·C for C ≥ 0.

HasAcceleratedRate from geometric decay

theorem PLAcceleratedNesterovLean.hasAcceleratedRate_of_geometric_decay {d : ℕ} (f : E d → ℝ) (iterates : ℕ → E d) (L μ L₀ r : ℝ) (hL₀ : 0 < L₀) (hr : 0 < r) (_hr1 : r < 1) (hrate : r ≤ Real.exp (-(1 / √(L / μ)))) (hbound : ∀ (k : ℕ), f (iterates k) - fStar f ≤ L₀ * r ^ k) : HasAcceleratedRate f iterates L μ

If f(xₖ) - f⋆ ≤ L₀ · rᵏ for r ∈ (0,1) where r ≤ exp(-1/√(L/μ)), then HasAcceleratedRate holds.