def IsGStar {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L : NNReal) : Prop

Definition 1.6.5 (1): an objective f : E → ℝ belongs to the textbook class 𝒢_* when f ∈ C^{1,1}_L and f is bounded below. Specializing E to ℝⁿ recovers the textbook formulation.

def GStarNotation.«term𝒢⋆[_]» : Lean.ParserDescr

@[simp]

theorem isGStar_iff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L : NNReal) : f ∈ {f : E → ℝ | IsGStar f L} ↔ ContDiff ℝ 1 f ∧ LipschitzWith L (gradient f) ∧ BddBelow (Set.range f)

Unfolding f ∈ 𝒢⋆[L] gives the canonical conjunction of C^{1,1}_L regularity and lower boundedness.

theorem IsGStar.contDiff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {L : NNReal} (h : f ∈ {f : E → ℝ | IsGStar f L}) : ContDiff ℝ 1 f

Membership in 𝒢_* supplies the C¹ regularity component of the objective.

theorem IsGStar.gradient_lipschitz {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {L : NNReal} (h : f ∈ {f : E → ℝ | IsGStar f L}) : LipschitzWith L (gradient f)

Membership in 𝒢_* supplies the global L-Lipschitz bound on the gradient.

theorem IsGStar.bddBelow {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {L : NNReal} (h : f ∈ {f : E → ℝ | IsGStar f L}) : BddBelow (Set.range f)

Membership in 𝒢_* supplies lower boundedness of the objective values.

theorem IsGStar.differentiableAt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {L : NNReal} (h : f ∈ {f : E → ℝ | IsGStar f L}) (x : E) : DifferentiableAt ℝ f x

Membership in 𝒢_* supplies ordinary differentiability at every point.

theorem IsGStar.hasGradientAt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {L : NNReal} (h : f ∈ {f : E → ℝ | IsGStar f L}) (x : E) : HasGradientAt f (gradient f x) x

Membership in 𝒢_* makes the displayed totalized gradient the genuine gradient.

def IsEpsilonSolution {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x0 : E) (ε : ℝ) (xBar : E) : Prop

A point x̄ is an ε-solution for an objective f relative to the starting point x₀ when f(x̄) ≤ f(x₀) and ‖∇ f(x̄)‖ ≤ ε. This source-facing stopping predicate lives on the plain objective f : E → ℝ; when f ∈ 𝒢⋆[L], the displayed gradient is source-faithful by IsGStar.hasGradientAt. Specializing E to ℝⁿ recovers the textbook formulation.

@[simp]

theorem isEpsilonSolution_iff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x0 xBar : E) (ε : ℝ) : IsEpsilonSolution f x0 ε xBar ↔ f xBar ≤ f x0 ∧ ‖gradient f xBar‖ ≤ ε

Unfolding IsEpsilonSolution f x₀ ε x̄ gives the textbook conditions f(x̄) ≤ f(x₀) and ‖∇ f(x̄)‖ ≤ ε.

noncomputable def gStarProblemClass (n : ℕ) (L : NNReal) (ε : ℝ) : BlackBoxOptimizationProblemClass (EuclideanSpace ℝ (Fin n)) (ℝ × EuclideanSpace ℝ (Fin n)) ({ f : EuclideanSpace ℝ (Fin n) → ℝ // f ∈ {f : EuclideanSpace ℝ (Fin n) → ℝ | IsGStar f L} } × EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n))

Definition 1.6.5 (2): the textbook class 𝒢_* at accuracy threshold ε, viewed as a Chapter 1 black-box optimization problem class. Its model is the subtype of lower-bounded unconstrained C^{1,1}_L(ℝⁿ) objectives, its oracle is the canonical first-order answer map x ↦ (f x, ∇ f x), and its stopping criterion accepts exactly the triples (f, x₀, x̄) for which x̄ is an ε-solution for the model objective f relative to x₀.

@[simp]

theorem gStarProblemClass_stops_iff {L : NNReal} {n : ℕ} {ε : ℝ} (f : { f : EuclideanSpace ℝ (Fin n) → ℝ // f ∈ {f : EuclideanSpace ℝ (Fin n) → ℝ | IsGStar f L} }) (x0 xBar : EuclideanSpace ℝ (Fin n)) : (f, x0, xBar) ∈ (gStarProblemClass n L ε).stoppingCriterion ↔ IsEpsilonSolution (↑f) x0 ε xBar

A state is accepted by gStarProblemClass n L ε exactly when its endpoint is an ε-solution for the model objective relative to its starting point.

@[simp]

theorem gStarProblemClass_oracle_apply {L : NNReal} {n : ℕ} {ε : ℝ} (f : { f : EuclideanSpace ℝ (Fin n) → ℝ // f ∈ {f : EuclideanSpace ℝ (Fin n) → ℝ | IsGStar f L} }) (x : EuclideanSpace ℝ (Fin n)) : (gStarProblemClass n L ε).oracle f x = (↑f x, gradient (↑f) x)

The oracle of gStarProblemClass n L ε is the canonical first-order answer map (f, x) ↦ (f x, ∇ f x).