theorem zero_model_smoothing_complexity_relation {E₁ : Type u} {E₂ : Type v} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] (A : E₁ →L[ℝ] StrongDual ℝ E₂) (f fμ : E₁ → ℝ) (φ : E₂ → ℝ) (N : ℕ+) (xN : E₁) (u : Fin (↑N + 1) → E₂) (D₁ D₂ ε : ℝ) (hε : 0 < ε) (hD₁ : 0 ≤ D₁) (hD₂ : 0 < D₂) (hxN_approx : fμ xN ≥ f xN - explicitModelSmoothingParameter A D₁ D₂ N * D₂) (hφ_le : φ (Finset.univ.centerMass (explicitModelDualAverageWeights ↑N) u) ≤ fμ xN) (hfμ_le : fμ xN ≤ f xN) (hsmoothed_gap : fμ xN - φ (Finset.univ.centerMass (explicitModelDualAverageWeights ↑N) u) ≤ 4 * ‖A‖ ^ 2 * D₁ / (explicitModelSmoothingParameter A D₁ D₂ N * (↑↑N * (↑↑N + 1)))) (hiter : 4 * ‖A‖ * √(D₁ * D₂) / ε ≤ √(↑↑N * (↑↑N + 1))) : f xN - φ (Finset.univ.centerMass (explicitModelDualAverageWeights ↑N) u) ≤ ε

Proposition 6.11: in the case M = 0, if the explicit-model smoothing hypotheses from Theorem 6.3 hold and √(N (N + 1)) ≥ 4 ‖A‖ √(D₁ D₂) / ε, then the primal-dual gap at (x_N, \hat u_N) is at most ε.