theorem primal_dual_decomposition_mem_Icc_of_gap_le {E : Type u} {U : Type v} {α : Type u_1} [AddCommGroup α] [Preorder α] [AddLeftMono α] [AddRightMono α] {f : E → α} {φ : U → α} {xN : E} {uHat : U} {fStar φStar rN : α} (h_primal : fStar ≤ f xN) (h_dual : φ uHat ≤ φStar) (h_weak_duality : φStar ≤ fStar) (h_gap : f xN - φ uHat ≤ rN) : f xN - fStar + (φStar - φ uHat) ∈ Set.Icc 0 (f xN - φ uHat) ∧ f xN - φ uHat ≤ rN

Lemma 3.1.23: if x_N satisfies the residual estimate (3.1.85), written here as f(x_N) - φ(\hat u_N) ≤ r_N, then the decomposition (f(x_N) - f^*) + (φ^* - φ(\hat u_N)) lies between 0 and the primal-dual gap f(x_N) - φ(\hat u_N), and that gap is itself bounded above by r_N.