noncomputable def constantStepSchemeIISimpleSetStep {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) : ↑QSet × E × ℝ → ↑QSet × E × ℝ

The one-step state update of Algorithm 2.7 on triples (x_k, y_k, α_k) with x_k ∈ Q.

noncomputable def constantStepSchemeIISimpleSet {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : ℕ → ↑QSet × E × ℝ

Algorithm 2.7: for a simple closed convex set Q, objective f, step parameter L, reciprocal condition number q_f, initial feasible point x₀ ∈ Q, and admissible initial scalar α₀ ∈ (√q_f, 2 (3 + q_f) / (3 + √(21 + 4 q_f))], the recursive state (x_k, y_k, α_k) starts from (x₀, x₀, α₀) and applies the projected step x_{k+1} = x_Q(y_k; L), the scalar update α_{k+1} = constantStepSchemeIIAlphaNext q_f α_k, and the textbook type-II momentum formula for y_{k+1}. The step parameter is stored at the owner level as the positive inverse-stepsize datum L : NNRealˣ, matching the projected-gradient owner API. The textbook ℝⁿ statement is the specialization E = EuclideanSpace ℝ (Fin n).

noncomputable def constantStepSchemeIISimpleSetX {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : ℕ → ↑QSet

The main iterate sequence x_k of the recursive simple-set type-II trajectory.

noncomputable def constantStepSchemeIISimpleSetY {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : ℕ → E

The extrapolated sequence y_k of the recursive simple-set type-II trajectory.

noncomputable def constantStepSchemeIISimpleSetAlpha {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : ℕ → ℝ

The scalar sequence α_k of the recursive simple-set type-II trajectory.

@[simp]

theorem constantStepSchemeIISimpleSet_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : constantStepSchemeIISimpleSet QSet hQ_closed hQ_convex f L qf x0 alpha0 0 = (x0, ↑x0, ↑alpha0)

@[simp]

theorem constantStepSchemeIISimpleSet_succ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) (k : ℕ) : constantStepSchemeIISimpleSet QSet hQ_closed hQ_convex f L qf x0 alpha0 (k + 1) = constantStepSchemeIISimpleSetStep QSet hQ_closed hQ_convex f L qf (constantStepSchemeIISimpleSet QSet hQ_closed hQ_convex f L qf x0 alpha0 k)

The recursive simple-set type-II state satisfies the one-step state update law.

@[simp]

theorem constantStepSchemeIISimpleSetX_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : constantStepSchemeIISimpleSetX QSet hQ_closed hQ_convex f L qf x0 alpha0 0 = x0

@[simp]

theorem constantStepSchemeIISimpleSetY_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : constantStepSchemeIISimpleSetY QSet hQ_closed hQ_convex f L qf x0 alpha0 0 = ↑x0

@[simp]

theorem constantStepSchemeIISimpleSetAlpha_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : constantStepSchemeIISimpleSetAlpha QSet hQ_closed hQ_convex f L qf x0 alpha0 0 = ↑alpha0

@[simp]

theorem constantStepSchemeIISimpleSetX_succ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) (k : ℕ) : ↑(constantStepSchemeIISimpleSetX QSet hQ_closed hQ_convex f L qf x0 alpha0 (k + 1)) = gradientMapping QSet ⋯ hQ_closed hQ_convex f (constantStepSchemeIISimpleSetY QSet hQ_closed hQ_convex f L qf x0 alpha0 k) L

The recursive simple-set type-II iterates satisfy the textbook projected step x_{k+1} = x_Q(y_k; L).

@[simp]

theorem constantStepSchemeIISimpleSetAlpha_succ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) (k : ℕ) : constantStepSchemeIISimpleSetAlpha QSet hQ_closed hQ_convex f L qf x0 alpha0 (k + 1) = constantStepSchemeIIAlphaNext qf (constantStepSchemeIISimpleSetAlpha QSet hQ_closed hQ_convex f L qf x0 alpha0 k)

The recursive simple-set type-II scalar sequence uses the canonical scheme-II update constantStepSchemeIIAlphaNext.

@[simp]

theorem constantStepSchemeIISimpleSetY_succ {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) (k : ℕ) : constantStepSchemeIISimpleSetY QSet hQ_closed hQ_convex f L qf x0 alpha0 (k + 1) = ↑(constantStepSchemeIISimpleSetX QSet hQ_closed hQ_convex f L qf x0 alpha0 (k + 1)) + (constantStepSchemeIISimpleSetAlpha QSet hQ_closed hQ_convex f L qf x0 alpha0 k * (1 - constantStepSchemeIISimpleSetAlpha QSet hQ_closed hQ_convex f L qf x0 alpha0 k) / (constantStepSchemeIISimpleSetAlpha QSet hQ_closed hQ_convex f L qf x0 alpha0 k ^ 2 + constantStepSchemeIISimpleSetAlpha QSet hQ_closed hQ_convex f L qf x0 alpha0 (k + 1))) • (↑(constantStepSchemeIISimpleSetX QSet hQ_closed hQ_convex f L qf x0 alpha0 (k + 1)) - ↑(constantStepSchemeIISimpleSetX QSet hQ_closed hQ_convex f L qf x0 alpha0 k))

The recursive simple-set type-II extrapolated points satisfy the textbook momentum update.

theorem constantStepSchemeIISimpleSetAlpha_mem_Ioo {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) (hqf : qf ∈ Set.Ico 0 1) (k : ℕ) : constantStepSchemeIISimpleSetAlpha QSet hQ_closed hQ_convex f L qf x0 alpha0 k ∈ Set.Ioo 0 1

If q_f ∈ [0, 1), then every scalar in the recursive simple-set type-II trajectory lies in (0, 1).

noncomputable def constantStepSchemeIISimpleSetToMomentumRecurrence {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (QSet : Set E) (hQ_closed : IsClosed QSet) (hQ_convex : Convex ℝ QSet) (f : E → ℝ) (L : NNRealˣ) (qf : ℝ) (x0 : ↑QSet) (alpha0 : ↑(Set.Ioc (√qf) (constantStepSchemeIIAlphaUpper qf))) : ConstantStepSchemeIIMomentumRecurrence E (↑QSet) qf x0 ↑alpha0

The recursive Algorithm 2.7 trajectory, viewed through the owner type-II momentum recurrence API.