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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.ms_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {M : ℝ} (hM : 0 < M) (g d : E) (hr : ‖g + M • d‖ ≤ M / 2 * ‖d‖) : inner ℝ g d ≤ -(3 * M / 8) * ‖d‖ ^ 2 - ‖g‖ ^ 2 / (2 * M)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.damped_step {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {M A a γ : ℝ} (hM : 0 < M) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (g x) x) (x z u w : E) (hA : 0 ≤ A) (ha : 0 < a) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hweight : γ * a ^ 2 * M ≤ A + a) (hr : have y := (A / (A + a)) • x + (a / (A + a)) • z; ‖g w + M • (w - y)‖ ≤ M / 2 * ‖w - y‖) : have y := (A / (A + a)) • x + (a / (A + a)) • z; have B := A + γ * a; have xnew := ((1 - γ) * A / B) • x + (γ * (A + a) / B) • w; B * (f xnew - f u) + 1 / 2 * ‖z - (γ * a) • g w - u‖ ^ 2 + γ * (A + a) * (3 * M / 8) * ‖w - y‖ ^ 2 ≤ A * (f x - f u) + 1 / 2 * ‖z - u‖ ^ 2