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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.gronwall_unit_bound {K c : ℝ} (hK : 0 ≤ K) (hc : 0 ≤ c) : gronwallBound 0 K c 1 ≤ c * Real.exp K

theorem LongTails.OracleTemplate.GeneralizedAccelerated.gradient_growth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 ≤ L0) (hL1 : 0 ≤ L1) (hg : Differentiable ℝ g) (hH : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (x y : E) : ‖g x - g y‖ ≤ (L0 + L1 * ‖g y‖) * Real.exp (L1 * ‖x - y‖) * ‖x - y‖

theorem LongTails.OracleTemplate.GeneralizedAccelerated.localCurvature_pos {E : Type u_1} [NormedAddCommGroup E] {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (g : E) : 0 < localCurvature L0 L1 g

theorem LongTails.OracleTemplate.GeneralizedAccelerated.local_step_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (y g : E) : ‖y - (1 / localCurvature L0 L1 g) • g - y‖ = ‖g‖ / localCurvature L0 L1 g

theorem LongTails.OracleTemplate.GeneralizedAccelerated.local_step_gradient_error {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hg : Differentiable ℝ g) (hH : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (y : E) : ‖g (y - (1 / localCurvature L0 L1 (g y)) • g y) - g y‖ ≤ ‖g y‖ / 2

theorem LongTails.OracleTemplate.GeneralizedAccelerated.local_step_residual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hg : Differentiable ℝ g) (hH : ∀ (x : E), ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (y : E) : have M := localCurvature L0 L1 (g y); have w := y - (1 / M) • g y; ‖g w + M • (w - y)‖ ≤ M / 2 * ‖w - y‖

theorem LongTails.OracleTemplate.GeneralizedAccelerated.local_step_movement {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 < L1) (y g : E) : localCurvature L0 L1 g ≤ 8 * L0 ∨ 1 / (8 * L1) ≤ ‖y - (1 / localCurvature L0 L1 g) • g - y‖