theorem primal_dual_decomposition_mem_Icc_and_gap_le_of_gap_le_max_delta {E : Type u} {U : Type v} {P : Set E} (δ : ℕ → E → ℝ) (hatf : ℕ → ℝ) (φ : U → ℝ) (uHat : ℕ → U) (fStar φStar : ℝ) (r : ℕ → ℝ) (h_primal_lower : ∀ (N : ℕ), fStar ≤ hatf N) (h_dual_upper_uHat : ∀ (N : ℕ), φ (uHat N) ≤ φStar) (h_weak_duality : φStar ≤ fStar) (δMax : ℕ → ℝ) (hδMax : ∀ (N : ℕ), IsGreatest (δ N '' P) (δMax N)) (h_gap_le_δMax : ∀ (N : ℕ), hatf N - φ (uHat N) ≤ δMax N) (h_δMax_le : ∀ (N : ℕ), δMax N ≤ r N) (N : ℕ) : (fun (N : ℕ) => hatf N - fStar + (φStar - φ (uHat N))) N ∈ Set.Icc 0 ((fun (N : ℕ) => hatf N - φ (uHat N)) N) ∧ (fun (N : ℕ) => hatf N - φ (uHat N)) N ≤ r N

Lemma 3.1.24: if the stagewise gap is bounded by an attained certificate maximum δMax N, and these maxima satisfy δMax N ≤ r_N, then for every stage N the decomposition (\hat f_N - f^*) + (\phi^* - φ(\hat u_N)) lies in the interval [0, \hat f_N - φ(\hat u_N)] and the gap itself is bounded by r_N.

theorem primal_dual_decomposition_mem_Icc_and_gap_le_of_gap_le_sSup_delta {E : Type u} {U : Type v} {P : Set E} (δ : ℕ → E → ℝ) (hatf : ℕ → ℝ) (φ : U → ℝ) (uHat : ℕ → U) (fStar φStar : ℝ) (r : ℕ → ℝ) (h_primal_lower : ∀ (N : ℕ), fStar ≤ hatf N) (h_dual_upper_uHat : ∀ (N : ℕ), φ (uHat N) ≤ φStar) (h_weak_duality : φStar ≤ fStar) (h_gap_le_sSup_delta : ∀ (N : ℕ), hatf N - φ (uHat N) ≤ sSup (δ N '' P)) (h_sSup_delta_le : ∀ (N : ℕ), sSup (δ N '' P) ≤ r N) (N : ℕ) : (fun (N : ℕ) => hatf N - fStar + (φStar - φ (uHat N))) N ∈ Set.Icc 0 ((fun (N : ℕ) => hatf N - φ (uHat N)) N) ∧ (fun (N : ℕ) => hatf N - φ (uHat N)) N ≤ r N

Companion canonical sSup reformulation of Lemma 3.1.24.

theorem primal_dual_gap_tendsto_zero_of_gap_le_sSup_delta {E : Type u} {U : Type v} {P : Set E} (δ : ℕ → E → ℝ) (hatf : ℕ → ℝ) (φ : U → ℝ) (uHat : ℕ → U) (fStar φStar : ℝ) (r : ℕ → ℝ) (h_primal_lower : ∀ (N : ℕ), fStar ≤ hatf N) (h_dual_upper_uHat : ∀ (N : ℕ), φ (uHat N) ≤ φStar) (h_weak_duality : φStar ≤ fStar) (h_gap_le_sSup_delta : ∀ (N : ℕ), hatf N - φ (uHat N) ≤ sSup (δ N '' P)) (h_sSup_delta_le : ∀ (N : ℕ), sSup (δ N '' P) ≤ r N) (hr_tendsto : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (N : ℕ) => hatf N - φ (uHat N)) Filter.atTop (nhds 0)

Companion canonical sSup convergence reformulation of Lemma 3.1.24.

theorem primal_dual_gap_tendsto_zero_of_gap_le_max_delta {E : Type u} {U : Type v} {P : Set E} (δ : ℕ → E → ℝ) (hatf : ℕ → ℝ) (φ : U → ℝ) (uHat : ℕ → U) (fStar φStar : ℝ) (r : ℕ → ℝ) (h_primal_lower : ∀ (N : ℕ), fStar ≤ hatf N) (h_dual_upper_uHat : ∀ (N : ℕ), φ (uHat N) ≤ φStar) (h_weak_duality : φStar ≤ fStar) (δMax : ℕ → ℝ) (hδMax : ∀ (N : ℕ), IsGreatest (δ N '' P) (δMax N)) (h_gap_le_δMax : ∀ (N : ℕ), hatf N - φ (uHat N) ≤ δMax N) (h_δMax_le : ∀ (N : ℕ), δMax N ≤ r N) (hr_tendsto : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (N : ℕ) => hatf N - φ (uHat N)) Filter.atTop (nhds 0)

If the stagewise gap in Lemma 3.1.24 is controlled by attained certificate maxima δMax N bounded by a sequence r_N converging to 0, then the primal-dual gap itself converges to 0.