theorem excessive_gap_bounds_primal_dual_errors {X : Type u} {U : Type v} {Q₁ : Set X} {Q₂ : Set U} {f fμ₂ : X → ℝ} {φ φμ₁ : U → ℝ} {xBar : X} {uBar : U} {fStar D₁ D₂ μ₁ μ₂ : ℝ} (h_primal : IsLeast (f '' Q₁) fStar) (h_dual : IsGreatest (φ '' Q₂) fStar) (hfμ₂_lower : f xBar - μ₂ * D₂ ≤ fμ₂ xBar) (hφμ₁_upper : φμ₁ uBar ≤ φ uBar + μ₁ * D₁) (hxBar : xBar ∈ Q₁) (huBar : uBar ∈ Q₂) (hexcessive_gap : satisfiesExcessiveGapCondition Q₁ Q₂ fμ₂ φμ₁ ⟨xBar, hxBar⟩ ⟨uBar, huBar⟩) : max (f xBar - fStar) (fStar - φ uBar) ∈ Set.Icc 0 (f xBar - φ uBar) ∧ f xBar - φ uBar ≤ μ₁ * D₁ + μ₂ * D₂

Lemma 6.6: if the primal value fStar is the minimum of f on Q₁, the same value is the maximum of φ on Q₂, and the local smoothing bounds together with the excessive-gap certificate hold at xBar ∈ Q₁ and uBar ∈ Q₂, then the primal and dual errors are both controlled by the raw duality gap, which is at most μ₁ D₁ + μ₂ D₂.