Retuning Parameters for Nesterov Algorithm

Defines both direct θ retuning parameters and phase-indexed auxiliary parameters for the Nesterov algorithm:

• Phase k (k ≥ 1): μₖ = μ·(1 − 4⁻ᵏ), θₖ = 4⁻ᵏ

Key arithmetic facts:

• μₖ ↑ μ as k → ∞
• θₖ ↓ 0 as k → ∞

Phase parameter definitions

noncomputable def PLAcceleratedNesterovLean.muOfPhase (μ : ℝ) (k : ℕ) : ℝ

PL parameter at phase k: μₖ = μ · (1 - (1/4)^k).

Equations

• PLAcceleratedNesterovLean.muOfPhase μ k = μ * (1 - 4⁻¹ ^ k)

noncomputable def PLAcceleratedNesterovLean.thetaOfPhase (k : ℕ) : ℝ

Budget-split parameter at phase k: θₖ = (1/4)^k.

Equations

• PLAcceleratedNesterovLean.thetaOfPhase k = 4⁻¹ ^ k

noncomputable def PLAcceleratedNesterovLean.rhoOfPhase (L μ : ℝ) (k : ℕ) : ℝ

Momentum parameter at phase k.

Equations

• PLAcceleratedNesterovLean.rhoOfPhase L μ k = (1 - √(PLAcceleratedNesterovLean.muOfPhase μ k / L)) / (1 + √(PLAcceleratedNesterovLean.muOfPhase μ k / L))

def PLAcceleratedNesterovLean.muOfTheta (μ θ : ℝ) : ℝ

Directly retuned PL parameter: μθ = μ · (1 - θ).

Equations

• PLAcceleratedNesterovLean.muOfTheta μ θ = μ * (1 - θ)

noncomputable def PLAcceleratedNesterovLean.rhoOfTheta (L μ θ : ℝ) : ℝ

Directly retuned momentum parameter.

Equations

• PLAcceleratedNesterovLean.rhoOfTheta L μ θ = (1 - √(PLAcceleratedNesterovLean.muOfTheta μ θ * (1 / L))) / (1 + √(PLAcceleratedNesterovLean.muOfTheta μ θ * (1 / L)))

noncomputable def PLAcceleratedNesterovLean.etaOfPhase (L : ℝ) : ℝ

Step size (constant across phases).

Equations

• PLAcceleratedNesterovLean.etaOfPhase L = 1 / L

Basic arithmetic properties

theorem PLAcceleratedNesterovLean.thetaOfPhase_pos (k : ℕ) : 0 < thetaOfPhase k

theorem PLAcceleratedNesterovLean.thetaOfPhase_lt_one {k : ℕ} (hk : 1 ≤ k) : thetaOfPhase k < 1

theorem PLAcceleratedNesterovLean.muOfPhase_pos {μ : ℝ} (hμ : 0 < μ) {k : ℕ} (hk : 1 ≤ k) : 0 < muOfPhase μ k

theorem PLAcceleratedNesterovLean.muOfTheta_pos {μ θ : ℝ} (hμ : 0 < μ) (hθ_lt1 : θ < 1) : 0 < muOfTheta μ θ

Positivity of the retuned parameter μθ.

theorem PLAcceleratedNesterovLean.muOfTheta_lt_mu {μ θ : ℝ} (hμ : 0 < μ) (hθ_pos : 0 < θ) : muOfTheta μ θ < μ

The retuned parameter is strictly below μ when θ > 0.

theorem PLAcceleratedNesterovLean.muOfPhase_lt_mu {μ : ℝ} (hμ : 0 < μ) (k : ℕ) : muOfPhase μ k < μ

theorem PLAcceleratedNesterovLean.muOfPhase_increasing {μ : ℝ} (hμ : 0 < μ) (k : ℕ) : muOfPhase μ k ≤ muOfPhase μ (k + 1)

theorem PLAcceleratedNesterovLean.muOfPhase_eq (μ : ℝ) (k : ℕ) : muOfPhase μ k = μ * (1 - thetaOfPhase k)

muOfPhase k = μ · (1 - θₖ)

theorem PLAcceleratedNesterovLean.one_sub_muOfPhase_div {μ : ℝ} (hμ : 0 < μ) (k : ℕ) : 1 - muOfPhase μ k / μ = thetaOfPhase k

1 - muOfPhase k / μ = θₖ

theorem PLAcceleratedNesterovLean.sqrt_muOfPhase_eta_le {μ η : ℝ} (hμ : 0 < μ) (hη : 0 < η) (k : ℕ) : √(muOfPhase μ k * η) ≤ √(μ * η)

a_k = √(μ_k·η) ≤ √(μ·η) for all k.

theorem PLAcceleratedNesterovLean.one_div_one_sub_sqrt_le {μ η : ℝ} (hμ : 0 < μ) (hη : 0 < η) (hμη : μ * η < 1) (k : ℕ) : 1 / (1 - √(muOfPhase μ k * η)) ≤ 1 / (1 - √(μ * η))

1/(1-a_k) ≤ 1/(1-√(μη)) for all k (uniform bound on jump constants).

Geometric series bounds

theorem PLAcceleratedNesterovLean.partial_geometric_sum_le {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (K : ℕ) : ∑ k ∈ Finset.range K, r ^ (k + 1) ≤ r / (1 - r)

Partial sums of r^(k+1) for 0 ≤ r < 1 are bounded by r/(1-r).

theorem PLAcceleratedNesterovLean.partial_geometric_half_le (K : ℕ) : ∑ k ∈ Finset.range K, (1 / 2) ^ (k + 1) ≤ 1

Partial sums of (1/2)^(k+1) are bounded by 1.

theorem PLAcceleratedNesterovLean.partial_geometric_quarter_le (K : ℕ) : ∑ k ∈ Finset.range K, (1 / 4) ^ (k + 1) ≤ 1 / 3

Partial sums of (1/4)^k for k ≥ 1 are bounded by 1/3.