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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.two_queries (p : Setups.GeneralizedSmoothAndConvex.Public) (g : p.E → p.E) (s : Iterate p.E) : (fun (state : (algorithm p).State 1) => (algorithm p).update 1 state (g ((algorithm p).query 1 state).2))^[2] (State.ready s) = State.ready (step p.L0 p.L1 g s)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.first_two_queries (p : Setups.GeneralizedSmoothAndConvex.Public) (g : p.E → p.E) (hL0 : 0 < p.L0) (hL1 : 0 ≤ p.L1) (hΔ : 0 < p.Δ) : (fun (state : (algorithm p).State 1) => (algorithm p).update 1 state (g ((algorithm p).query 1 state).2))^[2] ((algorithm p).initial 1 ()) = State.ready (step p.L0 p.L1 g (initialIterate p.L0 p.L1 p.R p.Δ p.x0 g))

theorem LongTails.OracleTemplate.GeneralizedAccelerated.execute_algorithm (p : Setups.GeneralizedSmoothAndConvex.Public) (g : p.E → p.E) (hL0 : 0 < p.L0) (hL1 : 0 ≤ p.L1) (hΔ : 0 < p.Δ) (N : ℕ) : (execute { seedSpace := fun (k : ℕ) => PUnit.instMeasurableSpace, law := ⟨MeasureTheory.Measure.dirac fun (x : ℕ) => (), ⋯⟩, answer := fun (x : ℕ) (x_1 : Fin 1 × p.E) (x_2 : Unit) => match x_1 with | (fst, x) => g x } (algorithm p) (fun (x : Fin 1) => 2 * N) () fun (x : ℕ) => ()) = (run p.L0 p.L1 g (initialIterate p.L0 p.L1 p.R p.Δ p.x0 g) N).x

theorem LongTails.OracleTemplate.GeneralizedAccelerated.execute_gradient_oracle (p : Setups.GeneralizedSmoothAndConvex.Public) (f : p.E → ℝ) (g : p.E → p.E) (oracle : Oracle p.E p.E) (hg : ∀ (x : p.E), HasGradientAt f (g x) x) (horacle : ∀ (k : ℕ) (seed : oracle.Seed 1 k) (x : p.E), HasGradientAt f (oracle.answer 1 k (0, x) seed) x) (hL0 : 0 < p.L0) (hL1 : 0 ≤ p.L1) (hΔ : 0 < p.Δ) (N : ℕ) (seed : (algorithm p).Seed 1) (oracleSeed : (k : ℕ) → oracle.Seed 1 k) : execute oracle (algorithm p) (fun (x : Fin 1) => 2 * N) seed oracleSeed = (run p.L0 p.L1 g (initialIterate p.L0 p.L1 p.R p.Δ p.x0 g) N).x