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

theorem LongTails.OracleTemplate.Gradient.execute_gd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (oracle : E → E) (L : ℝ) (x0 : E) (K : ℕ) : (execute { seedSpace := fun (k : ℕ) => PUnit.instMeasurableSpace, law := ⟨MeasureTheory.Measure.dirac fun (x : ℕ) => (), ⋯⟩, answer := fun (x : ℕ) (query : Fin 1 × E) (x_1 : Unit) => oracle query.2 } (gd (L, x0)) (fun (x : Fin 1) => K) () fun (x : ℕ) => ()) = (fun (x : E) => x - (1 / L) • oracle x)^[K] x0

theorem LongTails.OracleTemplate.Gradient.smooth_upper_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {oracle : E → E} {L : ℝ} (hg : ∀ (x : E), HasGradientAt f (oracle x) x) (hlip : ∀ (x y : E), ‖oracle x - oracle y‖ ≤ L * ‖x - y‖) (x y : E) : f y ≤ f x + inner ℝ (oracle x) (y - x) + L / 2 * ‖y - x‖ ^ 2

theorem LongTails.OracleTemplate.Gradient.convex_support {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {oracle : E → E} (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (oracle x) x) (x y : E) : inner ℝ (oracle x) (y - x) ≤ f y - f x

theorem LongTails.OracleTemplate.Gradient.descent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {oracle : E → E} {L : ℝ} (hL : 0 < L) (hg : ∀ (x : E), HasGradientAt f (oracle x) x) (hlip : ∀ (x y : E), ‖oracle x - oracle y‖ ≤ L * ‖x - y‖) (x : E) : f (x - (1 / L) • oracle x) ≤ f x - ‖oracle x‖ ^ 2 / (2 * L)

theorem LongTails.OracleTemplate.Gradient.gd_accuracy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (oracle : E → E) (L R ε : ℝ) (x0 xstar : E) (hL : 0 < L) (hR : 0 ≤ R) (hε : 0 < ε) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (oracle x) x) (hlip : ∀ (x y : E), ‖oracle x - oracle y‖ ≤ L * ‖x - y‖) (hdist : ‖x0 - xstar‖ ≤ R) (K : ℕ) (hbudget : max 1 ⌈L * R ^ 2 / (2 * ε)⌉₊ ≤ K) : f (execute { seedSpace := fun (k : ℕ) => PUnit.instMeasurableSpace, law := ⟨MeasureTheory.Measure.dirac fun (x : ℕ) => (), ⋯⟩, answer := fun (x : ℕ) (query : Fin 1 × E) (x_1 : Unit) => oracle query.2 } (gd (L, x0)) (fun (x : Fin 1) => K) () fun (x : ℕ) => ()) - f xstar ≤ ε