noncomputable def constantStepSchemeIAlphaNext (L mu gamma : ℝ) : ℝ

The canonical positive root of the optimal-method quadratic equation L * α^2 = (1 - α) * γ + α * μ.

theorem constantStepSchemeIAlphaNext_satisfies_equation {L mu gamma : ℝ} (hL : 0 < L) (hgamma : 0 < gamma) : L * constantStepSchemeIAlphaNext L mu gamma ^ 2 = (1 - constantStepSchemeIAlphaNext L mu gamma) * gamma + constantStepSchemeIAlphaNext L mu gamma * mu

Under L > 0 and γ > 0, the canonical root satisfies the defining optimal-method equation.

theorem constantStepSchemeIAlphaNext_pos {L mu gamma : ℝ} (hL : 0 < L) (hgamma : 0 < gamma) : 0 < constantStepSchemeIAlphaNext L mu gamma

The canonical root is positive whenever L > 0 and γ > 0.

theorem constantStepSchemeIAlphaNext_lt_one {L mu gamma : ℝ} (hL : 0 < L) (hmu : mu < L) (hgamma : 0 < gamma) : constantStepSchemeIAlphaNext L mu gamma < 1

If μ < L, then the canonical root lies strictly below 1.

theorem constantStepSchemeIAlphaNext_mem_Ioo {L mu gamma : ℝ} (hL : 0 < L) (hmu : mu < L) (hgamma : 0 < gamma) : constantStepSchemeIAlphaNext L mu gamma ∈ Set.Ioo 0 1

Under L > 0, μ < L, and γ > 0, the canonical root belongs to (0, 1).

noncomputable def constantStepSchemeI {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : ℕ → E × E × ℝ

Algorithm 2.3: the recursive type-I optimal-method trajectory. The primitive recursive state is (x_k, v_k, γ_k); the source-named quantities α_k and y_k are the canonical derived projections determined by step (a) and step (b).

noncomputable def constantStepSchemeIX {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : ℕ → E

The iterate sequence x_k of Algorithm 2.3.

noncomputable def constantStepSchemeIV {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : ℕ → E

The estimating-sequence centers v_k of Algorithm 2.3.

noncomputable def constantStepSchemeIGamma {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : ℕ → ℝ

The curvature sequence γ_k of Algorithm 2.3.

noncomputable def constantStepSchemeIAlpha {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : ℕ → ℝ

The coefficient sequence α_k of Algorithm 2.3, obtained from the canonical positive root of the quadratic step-(a) equation.

noncomputable def constantStepSchemeIY {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : ℕ → E

The interpolation sequence y_k of Algorithm 2.3.

@[simp]

theorem constantStepSchemeIX_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : constantStepSchemeIX f L mu x0 gamma0 0 = x0

@[simp]

theorem constantStepSchemeIV_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : constantStepSchemeIV f L mu x0 gamma0 0 = x0

@[simp]

theorem constantStepSchemeIGamma_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) : constantStepSchemeIGamma f L mu x0 gamma0 0 = gamma0

@[simp]

theorem constantStepSchemeIAlpha_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) (k : ℕ) : constantStepSchemeIAlpha f L mu x0 gamma0 k = constantStepSchemeIAlphaNext L mu (constantStepSchemeIGamma f L mu x0 gamma0 k)

theorem constantStepSchemeIY_eq {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) (k : ℕ) : constantStepSchemeIY f L mu x0 gamma0 k = (1 / (constantStepSchemeIGamma f L mu x0 gamma0 k + constantStepSchemeIAlpha f L mu x0 gamma0 k * mu)) • ((constantStepSchemeIAlpha f L mu x0 gamma0 k * constantStepSchemeIGamma f L mu x0 gamma0 k) • constantStepSchemeIV f L mu x0 gamma0 k + constantStepSchemeIGamma f L mu x0 gamma0 (k + 1) • constantStepSchemeIX f L mu x0 gamma0 k)

The interpolation sequence is given by the textbook weighted-average formula.

@[simp]

theorem constantStepSchemeIX_succ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) (k : ℕ) : constantStepSchemeIX f L mu x0 gamma0 (k + 1) = constantStepSchemeIY f L mu x0 gamma0 k - (1 / L) • gradient f (constantStepSchemeIY f L mu x0 gamma0 k)

The exact step-(c) update of Algorithm 2.3.

theorem constantStepSchemeIV_succ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) (k : ℕ) : constantStepSchemeIV f L mu x0 gamma0 (k + 1) = (1 / constantStepSchemeIGamma f L mu x0 gamma0 (k + 1)) • (((1 - constantStepSchemeIAlpha f L mu x0 gamma0 k) * constantStepSchemeIGamma f L mu x0 gamma0 k) • constantStepSchemeIV f L mu x0 gamma0 k + (constantStepSchemeIAlpha f L mu x0 gamma0 k * mu) • constantStepSchemeIY f L mu x0 gamma0 k - constantStepSchemeIAlpha f L mu x0 gamma0 k • gradient f (constantStepSchemeIY f L mu x0 gamma0 k))

The center update of Algorithm 2.3.

theorem constantStepSchemeIGamma_pos {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) {gamma0 : ℝ} (hL : 0 < L) (hgamma0 : 0 < gamma0) (k : ℕ) : 0 < constantStepSchemeIGamma f L mu x0 gamma0 k

The curvature sequence stays positive once γ₀ > 0 and L > 0.

theorem constantStepSchemeIAlpha_pos {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) {gamma0 : ℝ} (hL : 0 < L) (hgamma0 : 0 < gamma0) (k : ℕ) : 0 < constantStepSchemeIAlpha f L mu x0 gamma0 k

Every coefficient α_k is positive once γ₀ > 0 and L > 0.

theorem constantStepSchemeIAlpha_lt_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) {gamma0 : ℝ} (hL : 0 < L) (hmu : mu < L) (hgamma0 : 0 < gamma0) (k : ℕ) : constantStepSchemeIAlpha f L mu x0 gamma0 k < 1

Every coefficient α_k lies below 1 once μ < L.

theorem constantStepSchemeIAlpha_mem_Ioo {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) {gamma0 : ℝ} (hL : 0 < L) (hmu : mu < L) (hgamma0 : 0 < gamma0) (k : ℕ) : constantStepSchemeIAlpha f L mu x0 gamma0 k ∈ Set.Ioo 0 1

Every coefficient α_k belongs to (0, 1) under the canonical positivity hypotheses.

theorem constantStepSchemeIAlpha_equation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) {gamma0 : ℝ} (hL : 0 < L) (hgamma0 : 0 < gamma0) (k : ℕ) : L * constantStepSchemeIAlpha f L mu x0 gamma0 k ^ 2 = (1 - constantStepSchemeIAlpha f L mu x0 gamma0 k) * constantStepSchemeIGamma f L mu x0 gamma0 k + constantStepSchemeIAlpha f L mu x0 gamma0 k * mu

The recursive coefficients satisfy the optimal-method quadratic relation.

theorem constantStepSchemeIGamma_succ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) {gamma0 : ℝ} (hL : 0 < L) (hgamma0 : 0 < gamma0) (k : ℕ) : constantStepSchemeIGamma f L mu x0 gamma0 (k + 1) = (1 - constantStepSchemeIAlpha f L mu x0 gamma0 k) * constantStepSchemeIGamma f L mu x0 gamma0 k + constantStepSchemeIAlpha f L mu x0 gamma0 k * mu

The recursive curvature sequence satisfies the owner optimal-method update law.

theorem constantStepSchemeIX_succ_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {L mu : ℝ} {x0 : E} {gamma0 : ℝ} (hL : 0 < L) (hDiff : Differentiable ℝ f) (hGrad : LipschitzWith ⟨L, ⋯⟩ (gradient f)) (k : ℕ) : f (constantStepSchemeIX f L mu x0 gamma0 (k + 1)) ≤ f (constantStepSchemeIY f L mu x0 gamma0 k) - 1 / (2 * L) * ‖gradient f (constantStepSchemeIY f L mu x0 gamma0 k)‖ ^ 2

Under differentiability and L-Lipschitz gradient smoothness, the exact step of Algorithm 2.3 satisfies the owner descent inequality on the ambient real Hilbert space.

noncomputable def constantStepSchemeIToOptimalMethodRecurrence {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) (hL : 0 < L) (hmu_nonneg : 0 ≤ mu) (hmu : mu < L) (hgamma0 : 0 < gamma0) : OptimalMethodRecurrence f L mu x0 gamma0

The recursive Algorithm 2.3 trajectory, viewed through the owner optimal-method recurrence API.

noncomputable def constantStepSchemeIToGeneralOptimalMethodScheme {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (L mu : ℝ) (x0 : E) (gamma0 : ℝ) (hL : 0 < L) (hmu_nonneg : 0 ≤ mu) (hmu : mu < L) (hgamma0 : 0 < gamma0) (hDiff : Differentiable ℝ f) (hGrad : LipschitzWith ⟨L, ⋯⟩ (gradient f)) : GeneralOptimalMethodScheme f L mu x0 gamma0

Forgetting the exact step update and retaining the induced owner descent estimate yields the canonical GeneralOptimalMethodScheme.