theorem ConstrainedLevelMethod.full_step_increment_le_uniform_internal_iteration_bound {E : Type u} [PseudoMetricSpace E] (method : ConstrainedLevelMethodInput E) (hrelative : method.RelativeStoppingExists) (hfinite : method.SelectedThresholdFinite hrelative) (k : ℕ) (M_f D : ℝ) (hχ : 0 < method.chi) (hε : 0 < method.epsilon) (hα : method.levelCoefficient ∈ Set.Ioo 0 1) (hblock : ∀ {i p : ℕ}, i ≤ p → (history method hrelative hfinite k).gap p ≥ (1 - method.levelCoefficient) * (history method hrelative hfinite k).gap i → 0 < (history method hrelative hfinite k).gap p → ↑(p + 1 - i) ≤ M_f ^ 2 * D ^ 2 / ((1 - method.levelCoefficient) ^ 2 * (history method hrelative hfinite k).gap p ^ 2)) (hfull_step : method.epsilon ≤ (history method hrelative hfinite k).optimalValue (stoppingIndex method hrelative hfinite k)) : stoppingIndex method hrelative hfinite k ≤ levelMethodIterationCap M_f D (method.chi * method.epsilon) method.levelCoefficient

Lemma 3.3.9 (1): if master step k is a full step in the sense that the selected exact record value is still at least ε, and if the chapter owner hypotheses of Theorem 3.3.1 hold for the inner history method.history k, then the canonical full-step count j(k) - j(k - 1) represented by method.stoppingIndex k is bounded by the chapter owner levelMethodIterationCap evaluated at the uniform tolerance χ ε.

theorem ConstrainedLevelMethod.epsilon_le_optimalValue_pred_globalStopIndex {E : Type u} [PseudoMetricSpace E] (method : ConstrainedLevelMethodInput E) (hrelative : method.RelativeStoppingExists) (hfinite : method.SelectedThresholdFinite hrelative) {k : ℕ} (hstop : globallyStopsAt method hrelative hfinite k) (hglobal_pos : 0 < globalStopIndex method hrelative hfinite k hstop) : method.epsilon ≤ (history method hrelative hfinite k).optimalValue (globalStopIndex method hrelative hfinite k hstop - 1)

If the canonical global-stop index at master step k is positive, then the preceding exact record value is still above the global threshold ε.

theorem ConstrainedLevelMethod.chi_mul_epsilon_le_gap_pred_globalStopIndex {E : Type u} [PseudoMetricSpace E] (method : ConstrainedLevelMethodInput E) (hrelative : method.RelativeStoppingExists) (hfinite : method.SelectedThresholdFinite hrelative) {k : ℕ} (hstop : globallyStopsAt method hrelative hfinite k) (hchi_nonneg : 0 ≤ method.chi) (hglobal_pos : 0 < globalStopIndex method hrelative hfinite k hstop) (hglobal_le_stopping : globalStopIndex method hrelative hfinite k hstop ≤ stoppingIndex method hrelative hfinite k) : method.chi * method.epsilon ≤ (history method hrelative hfinite k).gap (globalStopIndex method hrelative hfinite k hstop - 1)

If the first global-stop index occurs no later than the canonical relative stopping index, then the predecessor gap is at least χ ε.

theorem ConstrainedLevelMethod.last_step_internal_iterations_le_uniform_internal_iteration_bound {E : Type u} [PseudoMetricSpace E] (method : ConstrainedLevelMethodInput E) (hrelative : method.RelativeStoppingExists) (hfinite : method.SelectedThresholdFinite hrelative) {k : ℕ} (hstop : globallyStopsAt method hrelative hfinite k) {M_f D : ℝ} (hχ : 0 < method.chi) (hε : 0 < method.epsilon) (hα : method.levelCoefficient ∈ Set.Ioo 0 1) (hglobal_pos : 0 < globalStopIndex method hrelative hfinite k hstop) (hglobal_le_stopping : globalStopIndex method hrelative hfinite k hstop ≤ stoppingIndex method hrelative hfinite k) (h_last_step_cap : ↑(globalStopIndex method hrelative hfinite k hstop) ≤ M_f ^ 2 * D ^ 2 / ((history method hrelative hfinite k).gap (globalStopIndex method hrelative hfinite k hstop - 1) ^ 2 * levelParameterObjective method.levelCoefficient)) : ↑(globalStopIndex method hrelative hfinite k hstop) ≤ constrainedLevelMethodInternalIterationBound M_f D method.chi method.epsilon method.levelCoefficient

Lemma 3.3.9 (2): if the final inner run at master step k globally stops at the canonical index globalStopIndex, if this global-stop index occurs no later than the canonical relative stopping index, and if the textbook predecessor-gap bound for that terminal run is available, then the number of internal iterations executed up to that globally stopping step is bounded by the displayed uniform chapter owner constrainedLevelMethodInternalIterationBound M_f D χ ε α.