theorem CompleteLevelMethod.optimalValue_le_comparison_add_of_complexity_estimate {E : Type u} [NormedAddCommGroup E] {problem : SetConstrainedMinimizationProblem E} (method : CompleteLevelMethod problem) {Mf : ℝ} {xStar : E} {ε : ℝ} {N : ℕ} (h_level_estimate : method.history.optimalValue N - problem.objective xStar ≤ 2 * Mf * ‖method.initialPoint - xStar‖ / √↑N) (hε : 0 < ε) (hN : 4 * Mf ^ 2 * ‖method.initialPoint - xStar‖ ^ 2 / ε ^ 2 ≤ ↑N) : method.history.optimalValue N ≤ problem.objective xStar + ε

Proposition 3.51, owner form: if a complete level-method run satisfies the standard estimate f_N^* - f(x*) ≤ 2 M_f ‖x₀ - x*‖ / √N on the owner sampled-prefix value f_N^* = fstar(method.history, N), then every budget N above 4 M_f² ‖x₀ - x*‖² / ε² forces f_N^* ≤ f(x*) + ε.

theorem CompleteLevelMethod.historyOptimalValue_le_optimalValue_add_of_complexity_estimate {E : Type u} [NormedAddCommGroup E] {problem : SetConstrainedMinimizationProblem E} (method : CompleteLevelMethod problem) {Mf : ℝ} {xStar : E} {ε : ℝ} {N : ℕ} (hxStar : xStar ∈ constrainedArgmin problem.feasibleSet problem.objective) (h_level_estimate : method.history.optimalValue N - problem.objective xStar ≤ 2 * Mf * ‖method.initialPoint - xStar‖ / √↑N) (hε : 0 < ε) (hN : 4 * Mf ^ 2 * ‖method.initialPoint - xStar‖ ^ 2 / ε ^ 2 ≤ ↑N) : ↑(method.history.optimalValue N) ≤ problem.optimalValue + ↑ε

Proposition 3.51, owner form: if x* is a constrained minimizer and the complete level method satisfies the standard comparison-point complexity estimate, then the sampled-prefix owner value f_N^* is within ε of the Chapter 1 constrained optimal value.

theorem CompleteLevelMethod.exists_isApproximateMinimizer_of_complexity_estimate {E : Type u} [NormedAddCommGroup E] {problem : SetConstrainedMinimizationProblem E} (method : CompleteLevelMethod problem) {Mf : ℝ} {xStar : E} {ε : ℝ} {N : ℕ} (hxStar : xStar ∈ constrainedArgmin problem.feasibleSet problem.objective) (h_level_estimate : method.history.optimalValue N - problem.objective xStar ≤ 2 * Mf * ‖method.initialPoint - xStar‖ / √↑N) (hε : 0 < ε) (hN : 4 * Mf ^ 2 * ‖method.initialPoint - xStar‖ ^ 2 / ε ^ 2 ≤ ↑N) : ∃ k ≤ N, problem.IsApproximateMinimizer ε (method.iterate k)

Proposition 3.51: under the same complexity budget, one of the iterates x₀, …, x_N of the complete level-method run is an ε-approximate minimizer of the constrained problem in the canonical Chapter 1 sense.

theorem CompleteLevelMethod.exists_isApproximateSolution_of_complexity_estimate {E : Type u} [NormedAddCommGroup E] {problem : SetConstrainedMinimizationProblem E} (method : CompleteLevelMethod problem) {Mf : ℝ} {xStar : E} {ε : ℝ} {N : ℕ} (hxStar : xStar ∈ constrainedArgmin problem.feasibleSet problem.objective) (h_level_estimate : method.history.optimalValue N - problem.objective xStar ≤ 2 * Mf * ‖method.initialPoint - xStar‖ / √↑N) (hε : 0 < ε) (hN : 4 * Mf ^ 2 * ‖method.initialPoint - xStar‖ ^ 2 / ε ^ 2 ≤ ↑N) : ∃ k ≤ N, IsApproximateSolution problem.objective xStar ε (method.iterate k)

The owner ε-minimizer conclusion of Proposition 3.51 recovers the textbook comparison-point form once the comparison point x* is known to lie in the constrained argmin set.