theorem primal_dual_gap_bound_of_smoothed_lower_approximation {Q₁ : Type u} {Q₂ : Type v} {f fμ₂ : Q₁ → ℝ} {φ : Q₂ → ℝ} {μ₂ D₂ r : ℝ} {xBar : Q₁} {uBar : Q₂} (happrox : f xBar - μ₂ * D₂ ≤ fμ₂ xBar) (hφ_le : φ uBar ≤ fμ₂ xBar) (hresidual : fμ₂ xBar - φ uBar ≤ r) (hsmoothed_le : fμ₂ xBar ≤ f xBar) : f xBar - φ uBar ∈ Set.Icc 0 (μ₂ * D₂ + r)

Lemma 6.12: if fμ₂ satisfies the local lower smoothing bound f xBar - μ₂ D₂ ≤ fμ₂ xBar, if φ uBar ≤ fμ₂ xBar ≤ f xBar, and if the residual smoothed gap fμ₂ xBar - φ uBar is bounded above by r, then the raw primal-dual gap at (xBar, uBar) lies in the interval [0, μ₂ D₂ + r].