noncomputable def stronglyConvexMultiStageAccelerationStageLength (kp : ℕ) (p : ℝ) (k : ℕ) : ℕ

The stage length t_{k+1} used at zero-based outer stage k in the multistage acceleration schedule, namely ⌈k_p / 2^{k / (2p)}⌉.

def StronglyConvexMultiStageAccelerationNotation.«termT[_;_]» : Lean.ParserDescr

theorem one_le_stronglyConvexMultiStageAccelerationStageLength {kp : ℕ} (hkp : 1 ≤ kp) (p : ℝ) (k : ℕ) : 1 ≤ stronglyConvexMultiStageAccelerationStageLength kp p k

Positive threshold indices produce positive stage lengths throughout the multistage schedule.

noncomputable def stronglyConvexMultiStageAccelerationTotalLowerLevelIterations (kp : ℕ) (p : ℝ) (T : ℕ) : ℕ

The total number of lower-level iterations performed during the first T stages of the multistage strategy.

def stronglyConvexMultiStageAccelerationOrbit {E : Type u} (innerIterate : ℕ → E → E) (kp : ℕ) (p : ℝ) (x0 : E) : ℕ → E

The outer-stage orbit (y_k) of the multistage strategy (5.2.28), started at x₀ and updated by running the inner method for the scheduled stage length ⌈k_p / 2^{k / (2p)}⌉ at each stage.

def StronglyConvexMultiStageAccelerationNotation.«termY[_|_;_;_]» : Lean.ParserDescr

Source-facing notation for the textbook outer-stage iterate y_k of the multistage strategy (5.2.28), with the ambient update map and schedule parameters explicit because they are not inferable from k alone.

@[simp]

theorem stronglyConvexMultiStageAccelerationOrbit_zero {E : Type u} (innerIterate : ℕ → E → E) (kp : ℕ) (p : ℝ) (x0 : E) : stronglyConvexMultiStageAccelerationOrbit innerIterate kp p x0 0 = x0

The multistage outer orbit starts at the prescribed point x₀.

@[simp]

theorem stronglyConvexMultiStageAccelerationOrbit_succ {E : Type u} (innerIterate : ℕ → E → E) (kp : ℕ) (p : ℝ) (x0 : E) (k : ℕ) : stronglyConvexMultiStageAccelerationOrbit innerIterate kp p x0 (k + 1) = innerIterate (stronglyConvexMultiStageAccelerationStageLength kp p k) (stronglyConvexMultiStageAccelerationOrbit innerIterate kp p x0 k)

The successor stage output is obtained by applying the prescribed ⌈k_p / 2^{k / (2p)}⌉-step inner run to the previous stage output.

def IsStronglyConvexMultiStageAccelerationStoppingStage {E : Type u} (innerIterate : ℕ → E → E) (Qf : Set E) (kp : ℕ) (p : ℝ) (x0 : E) (T : ℕ) : Prop

Definition 5.2.11: T is the stopping stage of the multistage acceleration strategy (5.2.28) when T is the first outer-stage index whose output lies in the terminal region Q_f.

@[simp]

theorem isStronglyConvexMultiStageAccelerationStoppingStage_iff {E : Type u} (innerIterate : ℕ → E → E) (Qf : Set E) (kp : ℕ) (p : ℝ) (x0 : E) (T : ℕ) : IsStronglyConvexMultiStageAccelerationStoppingStage innerIterate Qf kp p x0 T ↔ stronglyConvexMultiStageAccelerationOrbit innerIterate kp p x0 T ∈ Qf ∧ ∀ m < T, stronglyConvexMultiStageAccelerationOrbit innerIterate kp p x0 m ∉ Qf

Expanding IsStronglyConvexMultiStageAccelerationStoppingStage ... T says exactly that the outer orbit enters Q_f at stage T and not at any earlier stage.

theorem stronglyConvexMultiStageAccelerationStoppingStage_mem {E : Type u} {innerIterate : ℕ → E → E} {Qf : Set E} {kp : ℕ} {p : ℝ} {x0 : E} {T : ℕ} (hT : IsStronglyConvexMultiStageAccelerationStoppingStage innerIterate Qf kp p x0 T) : stronglyConvexMultiStageAccelerationOrbit innerIterate kp p x0 T ∈ Qf

The stopping-stage output lies in the terminal region Q_f.

theorem stronglyConvexMultiStageAcceleration_not_mem_of_lt_stoppingStage {E : Type u} {innerIterate : ℕ → E → E} {Qf : Set E} {kp T k : ℕ} {p : ℝ} {x0 : E} (hT : IsStronglyConvexMultiStageAccelerationStoppingStage innerIterate Qf kp p x0 T) (hk : k < T) : stronglyConvexMultiStageAccelerationOrbit innerIterate kp p x0 k ∉ Qf

Every stage strictly before a stopping stage lies outside the terminal region Q_f.

theorem one_le_of_isStronglyConvexMultiStageAccelerationStoppingStage_of_initial_not_mem {E : Type u} {innerIterate : ℕ → E → E} {Qf : Set E} {kp T : ℕ} {p : ℝ} {x0 : E} (hT : IsStronglyConvexMultiStageAccelerationStoppingStage innerIterate Qf kp p x0 T) (hx0 : x0 ∉ Qf) : 1 ≤ T

If the initial point lies outside Q_f, then every stopping stage is positive.