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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.root_log_le {A0 A : ℝ} (hA0 : 0 < A0) (hA : A0 ≤ A) : Real.log (2 * A ^ (1 / 3) / A0 ^ (1 / 3)) ≤ Real.log (2 * A / A0)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.high_log_simplify {A0 A a : ℝ} (hA0 : 0 < A0) (hA : A0 ≤ A) (ha : 0 ≤ a) : have β := 1 / (64 * (1 + a ^ (2 / 3))); 2 * Real.log (2 * A ^ (1 / 3) / A0 ^ (1 / 3)) / (β * (2 * Real.log 2 / 3)) ≤ 384 * (1 + a ^ (2 / 3)) * Real.log (2 * A / A0)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_count_positive {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) + 384 * (1 + (L1 * R) ^ (2 / 3)) * Real.log (2 * (run L0 L1 g s (n + 1)).A / s.A)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_count_smooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 : ℝ} (hL0 : 0 < L0) (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (hfirst : localCurvature L0 0 (g (coupling s)) = s.guess) (n : ℕ) : ↑n ≤ 96 * √(L0 * (run L0 0 g s (n + 1)).A)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_accuracy {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 / ε) + ↑⌈(L1 * R) ^ (2 / 3)⌉₊ * Real.log (4 + 4 * Δ / ε)) ≤ ↑N) : f (run L0 L1 g (initialIterate L0 L1 R Δ x0 g) N).x - f u ≤ ε