@[reducible, inline]

noncomputable abbrev initialLinearizationGapEReal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) : EReal

Auxiliary ambient Chapter 6 bridge for the Definition 6.54 gap: extend Ψ : Q → ℝ to E and take the corresponding chosen-dual EReal supremum.

noncomputable def initialLinearizationGapFamily {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) : ↑Q → ℝ

The feasible-point affine-composite gap family from Definition 6.54 at the initial point x₀, written with the canonical constrained gradient gradientWithin f Q x₀.

noncomputable def initialLinearizationGapSup {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) : ℝ

The real-valued supremum bridge attached to the Definition 6.54 affine-composite gap family. This is a companion bridge owner, not the main source-facing max_x quantity.

class InitialLinearizationGapMaximizer {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) : Type u

Auxiliary maximizing certificate for the textbook quantity V₀, represented by the canonical within-gradient at x₀ together with an attained maximum of the Definition 6.54 gap family.

• hasGradientWithinAt : HasGradientWithinAt f (gradientWithin f Q ↑x0) Q ↑x0

  The constrained gradient used in the definition is the actual displayed gradient datum.

• maximizer : ↑Q

  A feasible maximizer of the affine-composite gap family.

• isGreatest : IsGreatest (Set.range (initialLinearizationGapFamily Q f Ψ x0)) (initialLinearizationGapFamily Q f Ψ x0 (maximizer f Ψ x0))

  The chosen feasible point attains the textbook maximum.

@[implicit_reducible]

noncomputable instance instInitialLinearizationGapMaximizerX0 {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {Q : Set E} {f : E → ℝ} {Ψ : ↑Q → ℝ} (method : LinearOracleCompositeMethod Q f Ψ) : InitialLinearizationGapMaximizer Q f Ψ method.x0

A linear-oracle composite method supplies canonical maximizing data for the Definition 6.54 initial gap via the oracle point at iteration 0.

noncomputable def initialLinearizationGap {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) [hData : InitialLinearizationGapMaximizer Q f Ψ x0] : ℝ

The source-facing quantity V₀ from Definition 6.54 is the attained maximum of the feasible-point linearization gap at the starting point x₀, expressed using the canonical constrained gradient once the displayed gradient side condition and a maximizing feasible point are available. The same definition then introduces B_{ν,t} = a₀ V₀ + (\sum_{k=1}^t a_k^{1+ν} / A_k^ν) G_ν D^{1+ν}.

theorem initialLinearizationGap_hasGradientWithinAt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) [hData : InitialLinearizationGapMaximizer Q f Ψ x0] : HasGradientWithinAt f (gradientWithin f Q ↑x0) Q ↑x0

The maximizing data for V₀ include the gradient side condition needed for gradientWithin f Q x₀ to stand for the displayed gradient in Definition 6.54.

theorem initialLinearizationGap_isGreatest {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) [hData : InitialLinearizationGapMaximizer Q f Ψ x0] : IsGreatest (Set.range (initialLinearizationGapFamily Q f Ψ x0)) (initialLinearizationGap Q f Ψ x0)

The source-facing quantity V₀ is the greatest element of the Definition 6.54 gap family.

@[reducible, inline]

noncomputable abbrev initialLinearizationGapReal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) : ℝ

initialLinearizationGapReal is the real-supremum bridge attached to the Definition 6.54 gap family, retained as a companion name for compatibility with the old scalar-supremum surface.

theorem initialLinearizationGap_eq_oracleObjectiveGapSup {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) [hData : InitialLinearizationGapMaximizer Q f Ψ x0] : initialLinearizationGap Q f Ψ x0 = sSup (Set.range fun (x : ↑Q) => linearOptimizationOracleObjective ((InnerProductSpace.toDualMap ℝ E) (gradientWithin f Q ↑x0)) Ψ x0 - linearOptimizationOracleObjective ((InnerProductSpace.toDualMap ℝ E) (gradientWithin f Q ↑x0)) Ψ x)

The source-facing maximum V₀ agrees with the real supremum of the Chapter 6 oracle-objective drop family at the starting point.

theorem initialLinearizationGap_eq_linearizedCompositeGap {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) [hData : InitialLinearizationGapMaximizer Q f Ψ x0] : ↑(initialLinearizationGap Q f Ψ x0) = initialLinearizationGapEReal Q f Ψ x0

Definition 6.54: when the maximizing data certify the textbook maximum and displayed gradient at x₀, coercing the scalar source quantity V₀ to EReal agrees with the ambient chosen-dual gap owner linearizedCompositeGap, specialized to Function.extend Subtype.val Ψ 0.

theorem initialLinearizationGapReal_eq_oracleObjectiveGapSup {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) : initialLinearizationGapReal Q f Ψ x0 = sSup (Set.range fun (x : ↑Q) => linearOptimizationOracleObjective ((InnerProductSpace.toDualMap ℝ E) (gradientWithin f Q ↑x0)) Ψ x0 - linearOptimizationOracleObjective ((InnerProductSpace.toDualMap ℝ E) (gradientWithin f Q ↑x0)) Ψ x)

initialLinearizationGapReal is the real supremum bridge for the Chapter 6 oracle-objective drop family at the starting point, formed with the canonical constrained gradient gradientWithin f Q x₀.

theorem initialLinearizationGap_def {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) [hData : InitialLinearizationGapMaximizer Q f Ψ x0] : initialLinearizationGap Q f Ψ x0 = inner ℝ (gradientWithin f Q ↑x0) (↑x0 - ↑(InitialLinearizationGapMaximizer.maximizer f Ψ x0)) + Ψ x0 - Ψ (InitialLinearizationGapMaximizer.maximizer f Ψ x0)

Expanding the source-facing quantity V₀ at the chosen maximizing point gives the displayed affine-plus-regularizer gap value ⟪∇_Q f(x₀), x₀ - x⟫ + Ψ(x₀) - Ψ(x) from Definition 6.54.

theorem initialLinearizationGapReal_def {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) : initialLinearizationGapReal Q f Ψ x0 = sSup (Set.range fun (x : ↑Q) => inner ℝ (gradientWithin f Q ↑x0) (↑x0 - ↑x) + Ψ x0 - Ψ x)

Expanding the real-supremum bridge gives the supremum of the affine-plus-regularizer gap values ⟪∇_Q f(x₀), x₀ - x⟫ + Ψ(x₀) - Ψ(x) over x ∈ Q.

theorem initialLinearizationGapReal_eq_initialLinearizationGap {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (f : E → ℝ) (Ψ : ↑Q → ℝ) (x0 : ↑Q) [hData : InitialLinearizationGapMaximizer Q f Ψ x0] : initialLinearizationGapReal Q f Ψ x0 = initialLinearizationGap Q f Ψ x0

The real-supremum bridge agrees with the source-facing quantity V₀ when the maximum is attained.

@[reducible, inline]

noncomputable abbrev initialLinearizationErrorBound (V0 : ℝ) (a : ℕ → ℝ) (Gν D ν : ℝ) (t : ℕ) : ℝ

The Definition 6.54 error quantity B_{ν,t} attached to the scalar initial gap V₀. This is the same Chapter 6 owner as linearOptimizationOracleErrorBound; the present name only records its role in the source definition.

theorem initialLinearizationErrorBound_def (V0 : ℝ) (a : ℕ → ℝ) (Gν D ν : ℝ) (t : ℕ) : initialLinearizationErrorBound V0 a Gν D ν t = a 0 * V0 + (∑ k ∈ Finset.Icc 1 t, (a k).rpow (1 + ν) / (accumulatedWeights a k).rpow ν) * Gν * D.rpow (1 + ν)

Expanding initialLinearizationErrorBound V₀ a G_ν D ν t gives the exact Definition 6.54 formula for B_{ν,t} with A_k = A[a](k).