theorem algorithm311_duality_gap_bound {E1 : Type u_1} {E2 : Type u_2} [NormedAddCommGroup E1] [NormedSpace ℝ E1] [FiniteDimensional ℝ E1] [NormedAddCommGroup E2] [NormedSpace ℝ E2] [FiniteDimensional ℝ E2] (Q1 : Set E1) (Q2 : Set E2) (A : E1 →L[ℝ] E2 →L[ℝ] ℝ) (fhat : E1 → ℝ) (phihat : E2 → ℝ) (d1 : E1 → ℝ) (d2 : E2 → ℝ) (σ1 σ2 M D1 : ℝ) (xSeq ySeq : ℕ → ↑Q1) (uμ : E1 → E2) (N : ℕ) (hatu : ↑Q2) : have A' := { toFun := fun (x : E1) => ↑(A x), map_add' := ⋯, map_smul' := ⋯ }; have D2 := sSup (d2 '' Q2); have μ := 2 * OperatorNormDef A' / (↑N + 1) * √(D1 / (σ1 * σ2 * D2)); have fbar := SmoothedObjective Q2 A phihat d2 μ fhat; have f := fun (x : E1) => fhat x + sSup ((fun (u : E2) => (A x) u - phihat u) '' Q2); have φ := AdjointFormPotential Q1 Q2 A fhat phihat; LipschitzOnWith M.toNNReal (fun (x : E1) => fderiv ℝ fhat x) Q1 → 0 < σ1 → 0 < σ2 → StrongConvexOn Q1 σ1 d1 → StrongConvexOn Q2 σ2 d2 → IsProxDiameterBound Q1 d1 D1 → OptimalSchemeAlgorithm Q1 fbar d1 (M + 1 / (μ * σ2) * OperatorNormDef A' ^ 2) σ1 xSeq ySeq → (∀ (x : E1), IsSmoothedMaximizer Q2 A phihat d2 μ x (uμ x)) → ↑hatu = ∑ i ∈ Finset.range (N + 1), (2 * (↑i + 1) / ((↑N + 1) * (↑N + 2))) • uμ ↑(xSeq i) → ConvexOn ℝ Q1 fhat → DifferentiableOn ℝ fhat Q1 → ConvexOn ℝ Q2 phihat → (∀ (x : E1), fderiv ℝ (SmoothedMaxFunction Q2 A phihat d2 μ) x = LinearMap.toContinuousLinearMap ((AdjointOperator A') (uμ x))) → 0 ≤ M → 0 ≤ D1 → 0 < M + 1 / (μ * σ2) * OperatorNormDef A' ^ 2 → IsClosed Q1 → IsOpen Q1 → ConvexOn ℝ Q1 fbar → DifferentiableOn ℝ fbar Q1 → 0 ≤ μ → (∀ u ∈ Q2, 0 ≤ d2 u) → (∀ (x : E1), BddAbove ((fun (u : E2) => (A x) u - phihat u) '' Q2)) → BddAbove (d2 '' Q2) → Q2.Nonempty → (∀ (u : E2), BddBelow ((fun (x : E1) => (A x) u + fhat x) '' Q1)) → 0 ≤ f ↑(ySeq N) - φ hatu ∧ f ↑(ySeq N) - φ hatu ≤ 4 * OperatorNormDef A' / (↑N + 1) * √(D1 * D2 / (σ1 * σ2)) + 4 * M * D1 / (σ1 * (↑N + 1) ^ 2) ∧ ∀ ε > 0, ↑N ≥ 4 * OperatorNormDef A' / ε * √(D1 * D2 / (σ1 * σ2)) + 2 * √(M * D1 / (σ1 * ε)) → f ↑(ySeq N) - φ hatu ≤ ε

Theorem 1.4.1. Assume the structural model (2.2) and that fhat is differentiable with M-Lipschitz gradient on Q1. Let d1 be a prox-function of Q1 with parameter σ1 > 0 and prox-diameter D1 as in (4.3_D1). Let d2 be a prox-function of Q2 with strong convexity parameter σ2 > 0 and define D2 := max_{u ∈ Q2} d2 u as in Proposition 2.7. Apply Algorithm 3.11 to the smoothed problem (4.1) with μ = μ(N) = (2‖A‖_{1,2}/(N+1)) * sqrt(D1/(σ1 σ2 D2)) (equation (thm3_muN)). After N iterations define \hat x := y_N and \hat u := ∑_{i=0}^N 2(i+1)/((N+1)(N+2)) u_μ(x_i) (4.2). Then 0 ≤ f(\hat x) - φ(\hat u) and the duality-gap bound (4.3) holds, and consequently the ε-solution bound (4.4) holds.