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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.high_root_simplify {a D : ℝ} (ha : 0 ≤ a) (hD : 0 ≤ D) : 64 * (512 / 3 * a ^ 2 * D ^ 2) ^ (1 / 3) ≤ 512 * (a * D) ^ (2 / 3)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_count_self_normalized {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 R : ℝ} (hL0 : 0 < L0) (hL1 : 0 < L1) (hR : 0 ≤ R) (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) (hE : energy f u s ≤ R ^ 2) (hfirst : localCurvature L0 L1 (g (coupling s)) = s.guess) (n : ℕ) : ↑n ≤ 96 * √(L0 * (run L0 L1 g s (n + 1)).A) + 4 * Real.log (2 * (run L0 L1 g s (n + 1)).A / s.A) + 512 * (L1 * R * Real.log (2 * (run L0 L1 g s (n + 1)).A / s.A)) ^ (2 / 3)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_accuracy_self_normalized {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 R Δ ε : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hR : 0 < R) (hΔ : 0 < Δ) (hε : 0 < ε) (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‖) (x0 u : E) (hmin : IsMinOn f Set.univ u) (hdist : ‖x0 - u‖ ≤ R) (hgap : f x0 - f u ≤ Δ) (N : ℕ) (hN : 4096 * (1 + √(L0 * R ^ 2 / ε) + Real.log (4 + 4 * Δ / ε) + (L1 * R * Real.log (4 + 4 * Δ / ε)) ^ (2 / 3)) ≤ ↑N) : f (run L0 L1 g (initialIterate L0 L1 R Δ x0 g) N).x - f u ≤ ε

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_accuracy_min {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 R Δ ε : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hR : 0 < R) (hΔ : 0 < Δ) (hε : 0 < ε) (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‖) (x0 u : E) (hmin : IsMinOn f Set.univ u) (hdist : ‖x0 - u‖ ≤ R) (hgap : f x0 - f u ≤ Δ) (N : ℕ) (hN : 4096 * (1 + √(L0 * R ^ 2 / ε) + min (↑⌈(L1 * R) ^ (2 / 3)⌉₊ * Real.log (4 + 4 * Δ / ε)) (Real.log (4 + 4 * Δ / ε) + (L1 * R * Real.log (4 + 4 * Δ / ε)) ^ (2 / 3))) ≤ ↑N) : f (run L0 L1 g (initialIterate L0 L1 R Δ x0 g) N).x - f u ≤ ε