Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib.

theorem LongTails.OracleTemplate.GeneralizedAccelerated.tentativeWeight_pos {E : Type u_1} (s : Iterate E) (hguess : 0 < s.guess) : 0 < tentativeWeight s

theorem LongTails.OracleTemplate.GeneralizedAccelerated.tentativeWeight_equation {E : Type u_1} (s : Iterate E) (hA : 0 ≤ s.A) (hguess : 0 < s.guess) : s.guess * tentativeWeight s ^ 2 = s.A + tentativeWeight s

theorem LongTails.OracleTemplate.GeneralizedAccelerated.coupling_same {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A M : ℝ) (x : E) (hA : 0 ≤ A) (hM : 0 < M) : coupling { A := A, x := x, z := x, guess := M } = x

theorem LongTails.OracleTemplate.GeneralizedAccelerated.damping_bounds {M G : ℝ} (hM : 0 < M) (hG : 0 < G) : 0 < min 1 (G / M) ∧ min 1 (G / M) ≤ 1 ∧ min 1 (G / M) * M ≤ G

theorem LongTails.OracleTemplate.GeneralizedAccelerated.finish_uniform {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : Pending E) (g : E) (hA : 0 ≤ p.previous.A) (ha : 0 < p.weight) (hM : 0 < p.curvature) (hG : 0 < p.previous.guess) : have γ := min 1 (p.previous.guess / p.curvature); have B := p.previous.A + γ * p.weight; (finish p g).A = B ∧ (finish p g).x = ((1 - γ) * p.previous.A / B) • p.previous.x + (γ * (p.previous.A + p.weight) / B) • p.point ∧ (finish p g).z = p.previous.z - (γ * p.weight) • g ∧ 0 < (finish p g).guess

theorem LongTails.OracleTemplate.GeneralizedAccelerated.step_weights {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) : have M := localCurvature L0 L1 (g (coupling s)); have γ := min 1 (s.guess / M); (step L0 L1 g s).A = s.A + γ * tentativeWeight s ∧ s.A < (step L0 L1 g s).A ∧ (step L0 L1 g s).A ≤ s.A + tentativeWeight s ∧ 0 < (step L0 L1 g s).guess

theorem LongTails.OracleTemplate.GeneralizedAccelerated.down_growth {G A a : ℝ} (hG : 0 < G) (hA : 0 ≤ A) (ha : 0 < a) (he : G * a ^ 2 = A + a) : 1 / (2 * √G) ≤ √(A + a) - √A

theorem LongTails.OracleTemplate.GeneralizedAccelerated.step_energy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (g x) x) (hgd : Differentiable ℝ g) (hH : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (s : Iterate E) (u : E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) : have y := coupling s; have M := localCurvature L0 L1 (g y); have w := y - (1 / M) • g y; have γ := min 1 (s.guess / M); have next := step L0 L1 g s; next.A * (f next.x - f u) + 1 / 2 * ‖next.z - u‖ ^ 2 + γ * (s.A + tentativeWeight s) * (3 * M / 8) * ‖w - y‖ ^ 2 ≤ s.A * (f s.x - f u) + 1 / 2 * ‖s.z - u‖ ^ 2

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.energy {E : Type u_1} [NormedAddCommGroup E] (f : E → ℝ) (u : E) (s : Iterate E) : ℝ

The objective-gap and squared-distance potential for accelerated convergence.

Equations

• LongTails.OracleTemplate.GeneralizedAccelerated.energy f u s = s.A * (f s.x - f u) + 1 / 2 * ‖s.z - u‖ ^ 2

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.dissipation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L0 L1 : ℝ) (g : E → E) (s : Iterate E) : ℝ

The nonnegative energy decrease charged to one accelerated step.

Equations

• One or more equations did not get rendered due to their size.

theorem LongTails.OracleTemplate.GeneralizedAccelerated.dissipation_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) : 0 ≤ dissipation L0 L1 g s

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_valid {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (n : ℕ) : 0 ≤ (run L0 L1 g s n).A ∧ 0 < (run L0 L1 g s n).guess

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_energy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (g x) x) (hgd : Differentiable ℝ g) (hH : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (s : Iterate E) (u : E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (n : ℕ) : energy f u (run L0 L1 g s n) + ∑ k ∈ Finset.range n, dissipation L0 L1 g (run L0 L1 g s k) ≤ energy f u s

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_weight_mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) : Monotone fun (n : ℕ) => (run L0 L1 g s n).A

theorem LongTails.OracleTemplate.GeneralizedAccelerated.step_guess {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (s : Iterate E) : (step L0 L1 g s).guess = if localCurvature L0 L1 (g (coupling s)) ≤ s.guess then s.guess / 16 else 16 * s.guess

theorem LongTails.OracleTemplate.GeneralizedAccelerated.step_inverse_sqrt_guess {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (s : Iterate E) (hG : 0 < s.guess) : 1 / √(step L0 L1 g s).guess = if localCurvature L0 L1 (g (coupling s)) ≤ s.guess then 4 * (1 / √s.guess) else 1 / √s.guess / 4

theorem LongTails.OracleTemplate.GeneralizedAccelerated.step_down_growth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (hdown : localCurvature L0 L1 (g (coupling s)) ≤ s.guess) : 1 / (2 * √s.guess) ≤ √(step L0 L1 g s).A - √s.A

theorem LongTails.OracleTemplate.GeneralizedAccelerated.down_sum_le_sqrt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (N : ℕ) : (∑ i ∈ Finset.range N, if localCurvature L0 L1 (g (coupling (run L0 L1 g s i))) ≤ (run L0 L1 g s i).guess then 1 / √(run L0 L1 g s i).guess else 0) ≤ 2 * √(run L0 L1 g s N).A

theorem LongTails.OracleTemplate.GeneralizedAccelerated.step_high_dissipation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 < L1) (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (hup : s.guess ≤ localCurvature L0 L1 (g (coupling s))) (hhigh : 8 * L0 < localCurvature L0 L1 (g (coupling s))) : (step L0 L1 g s).A * s.guess ≤ 512 / 3 * L1 ^ 2 * dissipation L0 L1 g s

theorem LongTails.OracleTemplate.GeneralizedAccelerated.initial_energy {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} {g : E → E} {L0 L1 R Δ : ℝ} (hΔ : 0 < Δ) (x0 u : E) (hdist : ‖x0 - u‖ ≤ R) (hgap : f x0 - f u ≤ Δ) : energy f u (initialIterate L0 L1 R Δ x0 g) ≤ R ^ 2

theorem LongTails.OracleTemplate.GeneralizedAccelerated.energy_nonneg {E : Type u_1} [NormedAddCommGroup E] {f : E → ℝ} {u : E} (hmin : IsMinOn f Set.univ u) (s : Iterate E) (hA : 0 ≤ s.A) : 0 ≤ energy f u s

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_dissipation_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (g x) x) (hgd : Differentiable ℝ g) (hH : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (s : Iterate E) (u : E) (hmin : IsMinOn f Set.univ u) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (N : ℕ) : ∑ i ∈ Finset.range N, dissipation L0 L1 g (run L0 L1 g s i) ≤ energy f u s

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_high_sum_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 < L1) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (g x) x) (hgd : Differentiable ℝ g) (hH : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (s : Iterate E) (u : E) (hmin : IsMinOn f Set.univ u) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (N : ℕ) (Q : Finset ℕ) (hQ : Q ⊆ Finset.range N) (hup : ∀ i ∈ Q, (run L0 L1 g s i).guess ≤ localCurvature L0 L1 (g (coupling (run L0 L1 g s i)))) (hhigh : ∀ i ∈ Q, 8 * L0 < localCurvature L0 L1 (g (coupling (run L0 L1 g s i)))) : ∑ i ∈ Q, (run L0 L1 g s (i + 1)).A * (run L0 L1 g s i).guess ≤ 512 / 3 * L1 ^ 2 * energy f u s

theorem LongTails.OracleTemplate.GeneralizedAccelerated.initial_first_down {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 R Δ : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hΔ : 0 < Δ) (x0 : E) : have s := initialIterate L0 L1 R Δ x0 g; localCurvature L0 L1 (g (coupling s)) = s.guess

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_weight_le_of_inaccurate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 R ε : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (g x) x) (hgd : Differentiable ℝ g) (hH : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (s : Iterate E) (u : E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (hE : energy f u s ≤ R ^ 2) (hε : 0 < ε) (N : ℕ) (hfail : ε < f (run L0 L1 g s N).x - f u) : (run L0 L1 g s N).A ≤ R ^ 2 / ε

A failed target accuracy bounds the accumulated weight using the common energy estimate.