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

structure LongTails.Setups.SmoothAndConvex.Public : Type (u + 1)

Problem information available to the method, excluding its target accuracy.

• E : Type u

  Real Hilbert space in which optimization takes place.

• normedE : NormedAddCommGroup self.E

  Normed additive structure of the optimization space.

• linearE : InnerProductSpace ℝ self.E

  Real inner product defining gradients.

• completeE : CompleteSpace self.E

  Completeness of the optimization space.

• L : ℝ

  Global Lipschitz bound for the gradient.

• x0 : self.E

  Initial point of the algorithm.

structure LongTails.Setups.SmoothAndConvex.Paramsextends LongTails.Setups.SmoothAndConvex.Public : Type (u_1 + 1)

Public problem information together with the parameters of the accuracy guarantee.

• E : Type u_1
• normedE : NormedAddCommGroup self.E
• linearE : InnerProductSpace ℝ self.E
• completeE : CompleteSpace self.E
• L : ℝ
• x0 : self.E
• R : ℝ

  Bound on the initial distance to a minimizer.

• ε : ℝ

  Positive target objective-gap accuracy.

@[reducible, inline]

abbrev LongTails.Setups.SmoothAndConvex.spec : OracleTemplate.Setup

Convex optimization with exact gradients and the displayed regularity assumptions.

Equations

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