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

structure LongTails.OracleTemplate.GeneralizedAccelerated.Iterate (E : Type u_1) : Type u_1

The reported point, auxiliary center, accumulated weight and curvature guess.

• A : ℝ

  Accumulated accelerated weight.

• x : E

  Point reported after the step.

• z : E

  Auxiliary center in the energy potential.

• guess : ℝ

  Current estimate of the local curvature.

structure LongTails.OracleTemplate.GeneralizedAccelerated.Pending (E : Type u_1) : Type u_1

A first gradient query and the state needed to consume the second query.

• previous : Iterate E

  Iterate before the current pair of queries.

• weight : ℝ

  Tentative accelerated weight.

• y : E

  Interpolation point used for the first query.

• curvature : ℝ

  Curvature computed from the first gradient.

• point : E

  Local step at which the second gradient is queried.

inductive LongTails.OracleTemplate.GeneralizedAccelerated.State (E : Type u_1) : Type u_1

The initialization, first-query and second-query phases of the accelerated algorithm.

• start {E : Type u_1} (A : ℝ) (x : E) : State E
• ready {E : Type u_1} (s : Iterate E) : State E
• pending {E : Type u_1} (p : Pending E) : State E

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.tentativeWeight {E : Type u_1} (s : Iterate E) : ℝ

The positive root of the accelerated weight equation for a curvature guess.

Equations

• LongTails.OracleTemplate.GeneralizedAccelerated.tentativeWeight s = (1 + √(1 + 4 * s.guess * s.A)) / (2 * s.guess)

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.coupling {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Iterate E) : E

The weighted interpolation of the reported point and auxiliary center.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.localCurvature {E : Type u_1} [NormedAddCommGroup E] (L0 L1 : ℝ) (g : E) : ℝ

A gradient-dependent curvature bound used to choose a safe local step.

Equations

• LongTails.OracleTemplate.GeneralizedAccelerated.localCurvature L0 L1 g = 4 * (L0 + L1 * ‖g‖)

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.prepare {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L0 L1 : ℝ) (s : Iterate E) (y g : E) : Pending E

Form a local gradient step and retain its data for the second gradient query.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.finish {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : Pending E) (g : E) : Iterate E

Consume the second gradient, damping the update when the curvature guess is too small.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.step {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L0 L1 : ℝ) (g : E → E) (s : Iterate E) : Iterate E

One accelerated step, using gradients at the interpolation point and the local step.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.initialIterate {E : Type u_1} [NormedAddCommGroup E] (L0 L1 R Δ : ℝ) (x0 : E) (g : E → E) : Iterate E

Initialize the energy weight from the radius and objective-gap bounds.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.run {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L0 L1 : ℝ) (g : E → E) (s : Iterate E) : ℕ → Iterate E

The accelerated iterate after a fixed number of two-gradient steps.

Equations

• One or more equations did not get rendered due to their size.
• LongTails.OracleTemplate.GeneralizedAccelerated.run L0 L1 g s 0 = s

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.algorithm (p : Setups.GeneralizedSmoothAndConvex.Public) : Algorithm p.E p.E p.E

The oracle state machine implementing damped acceleration without objective queries.

Equations

• One or more equations did not get rendered due to their size.