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

structure LongTails.Setups.GeneralizedSmoothAndConvex.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.

• L0 : ℝ

  Constant part of the Hessian-growth bound.

• L1 : ℝ

  Coefficient of gradient norm in the Hessian-growth bound.

• R : ℝ

  Bound on initial distance to an attained minimizer.

• Δ : ℝ

  Bound on the initial objective gap.

• x0 : self.E

  Initial point of the algorithm.

structure LongTails.Setups.GeneralizedSmoothAndConvex.Paramsextends LongTails.Setups.GeneralizedSmoothAndConvex.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
• L0 : ℝ
• L1 : ℝ
• R : ℝ
• Δ : ℝ
• x0 : self.E
• ε : ℝ

  Positive target objective-gap accuracy.

@[reducible, inline]

abbrev LongTails.Setups.GeneralizedSmoothAndConvex.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.