def gapFunctionCertificate {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {N : ℕ} (y : Fin (N + 1) → V) (α : Fin (N + 1) → ℝ) (g : V → V) : V → ℝ

The gap-function certificate δ_N(x) = ∑_{k=0}^N α_k ⟪g(y_k), y_k - x⟫.

theorem gapFunctionCertificate_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {N : ℕ} (y : Fin (N + 1) → V) (α : Fin (N + 1) → ℝ) (g : V → V) (x : V) : gapFunctionCertificate y α g x = ∑ k : Fin (N + 1), α k * inner ℝ (g (y k)) (y k - x)

Evaluating gapFunctionCertificate at x gives the defining finite sum ∑_{k=0}^N α_k ⟪g(y_k), y_k - x⟫.

theorem weightedPrimalDualGap_le_sSup_gapFunctionCertificate {E : Type u} {U : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [AddCommGroup U] [Module ℝ U] {P : Set E} {ψ : E → U → ℝ} {g : E → E} (y : (N : ℕ) → Fin (N + 1) → E) (u : (N : ℕ) → Fin (N + 1) → U) (α : (N : ℕ) → Fin (N + 1) → ℝ) (hP_nonempty : P.Nonempty) (hlower_bddBelow : ∀ (N : ℕ), BddBelow ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P)) (hα_nonneg : ∀ (N : ℕ) (k : Fin (N + 1)), 0 ≤ α N k) (hα_sum_one : ∀ (N : ℕ), ∑ k : Fin (N + 1), α N k = 1) (hsubgradient_uHat : ∀ (N : ℕ) (k : Fin (N + 1)), ∀ x ∈ P, ψ (y N k) (Finset.univ.centerMass (α N) (u N)) - ψ x (Finset.univ.centerMass (α N) (u N)) ≤ inner ℝ (g (y N k)) (y N k - x)) (haggregate : ∀ (N : ℕ), (α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) ≤ ∑ k : Fin (N + 1), α N k * ψ (y N k) (Finset.univ.centerMass (α N) (u N))) (hδ_bddAbove : ∀ (N : ℕ), BddAbove ((fun (N : ℕ) => gapFunctionCertificate (y N) (α N) g) N '' P)) (N : ℕ) : (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) N ≤ sSup ((fun (N : ℕ) => gapFunctionCertificate (y N) (α N) g) N '' P)

Bridge theorem: the weighted primal-dual gap is bounded by the supremum of the certificate image on P. This is the canonical sSup form of the source certificate estimate, before any explicit residual sequence r_N is inserted.

theorem weightedPrimalDualGap_le_of_gapFunctionCertificate_bound {E : Type u} {U : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [AddCommGroup U] [Module ℝ U] {P : Set E} {ψ : E → U → ℝ} {g : E → E} (y : (N : ℕ) → Fin (N + 1) → E) (u : (N : ℕ) → Fin (N + 1) → U) (α : (N : ℕ) → Fin (N + 1) → ℝ) (r : ℕ → ℝ) (hP_nonempty : P.Nonempty) (hlower_bddBelow : ∀ (N : ℕ), BddBelow ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P)) (hα_nonneg : ∀ (N : ℕ) (k : Fin (N + 1)), 0 ≤ α N k) (hα_sum_one : ∀ (N : ℕ), ∑ k : Fin (N + 1), α N k = 1) (hsubgradient_uHat : ∀ (N : ℕ) (k : Fin (N + 1)), ∀ x ∈ P, ψ (y N k) (Finset.univ.centerMass (α N) (u N)) - ψ x (Finset.univ.centerMass (α N) (u N)) ≤ inner ℝ (g (y N k)) (y N k - x)) (haggregate : ∀ (N : ℕ), (α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) ≤ ∑ k : Fin (N + 1), α N k * ψ (y N k) (Finset.univ.centerMass (α N) (u N))) (hdelta : ∀ (N : ℕ), ∀ x ∈ P, (fun (N : ℕ) => gapFunctionCertificate (y N) (α N) g) N x ≤ r N) (N : ℕ) : (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) N ≤ r N

Bridge theorem from pointwise certificate control to the raw gap bound. This is not the main source-facing statement of Lemma 3.24; it is the residual-bound corollary obtained by combining the sSup bridge above with the pointwise estimate δ_N(x) ≤ r_N.

theorem primal_dual_decomposition_mem_Icc_and_gap_le_of_gapFunctionCertificate_max {E : Type u} {U : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [AddCommGroup U] [Module ℝ U] {P : Set E} {ψ : E → U → ℝ} {g : E → E} (y : (N : ℕ) → Fin (N + 1) → E) (u : (N : ℕ) → Fin (N + 1) → U) (α : (N : ℕ) → Fin (N + 1) → ℝ) (r : ℕ → ℝ) (hP_nonempty : P.Nonempty) (hlower_bddBelow : ∀ (N : ℕ), BddBelow ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P)) (hα_nonneg : ∀ (N : ℕ) (k : Fin (N + 1)), 0 ≤ α N k) (hα_sum_one : ∀ (N : ℕ), ∑ k : Fin (N + 1), α N k = 1) (hsubgradient_uHat : ∀ (N : ℕ) (k : Fin (N + 1)), ∀ x ∈ P, ψ (y N k) (Finset.univ.centerMass (α N) (u N)) - ψ x (Finset.univ.centerMass (α N) (u N)) ≤ inner ℝ (g (y N k)) (y N k - x)) (haggregate : ∀ (N : ℕ), (α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) ≤ ∑ k : Fin (N + 1), α N k * ψ (y N k) (Finset.univ.centerMass (α N) (u N))) (fStar φStar : ℝ) (h_primal_lower : ∀ (N : ℕ), fStar ≤ α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) (h_dual_upper_uHat : ∀ (N : ℕ), sInf ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P) ≤ φStar) (h_weak_duality : φStar ≤ fStar) (δMax : ℕ → ℝ) (hδMax : ∀ (N : ℕ), IsGreatest ((fun (N : ℕ) => gapFunctionCertificate (y N) (α N) g) N '' P) (δMax N)) (hδMax_le : ∀ (N : ℕ), δMax N ≤ r N) (N : ℕ) : (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - fStar + (φStar - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N))) N ∈ Set.Icc 0 ((fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) N) ∧ (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) N ≤ r N

Lemma 3.24: if the weighted primal-dual gap is controlled by the attained certificate maximum max_{x ∈ P} δ_N(x) and these maxima are bounded above by r_N, then for every stage N the source decomposition (\hat f_N - f^*) + (\phi^* - inf_{x ∈ P} ψ(x, \hat u_N)) with \hat f_N = dotProduct (α N) (fun k ↦ ψ (y N k) (u N k)) and \hat u_N = (Finset.univ).centerMass (α N) (u N) lies in the interval [0, \hat f_N - inf_{x ∈ P} ψ(x, \hat u_N)], and that gap is bounded above by r_N.

theorem primal_dual_decomposition_mem_Icc_and_gap_le_of_gapFunctionCertificate_sSup {E : Type u} {U : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [AddCommGroup U] [Module ℝ U] {P : Set E} {ψ : E → U → ℝ} {g : E → E} (y : (N : ℕ) → Fin (N + 1) → E) (u : (N : ℕ) → Fin (N + 1) → U) (α : (N : ℕ) → Fin (N + 1) → ℝ) (r : ℕ → ℝ) (hP_nonempty : P.Nonempty) (hlower_bddBelow : ∀ (N : ℕ), BddBelow ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P)) (hα_nonneg : ∀ (N : ℕ) (k : Fin (N + 1)), 0 ≤ α N k) (hα_sum_one : ∀ (N : ℕ), ∑ k : Fin (N + 1), α N k = 1) (hsubgradient_uHat : ∀ (N : ℕ) (k : Fin (N + 1)), ∀ x ∈ P, ψ (y N k) (Finset.univ.centerMass (α N) (u N)) - ψ x (Finset.univ.centerMass (α N) (u N)) ≤ inner ℝ (g (y N k)) (y N k - x)) (haggregate : ∀ (N : ℕ), (α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) ≤ ∑ k : Fin (N + 1), α N k * ψ (y N k) (Finset.univ.centerMass (α N) (u N))) (fStar φStar : ℝ) (h_primal_lower : ∀ (N : ℕ), fStar ≤ α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) (h_dual_upper_uHat : ∀ (N : ℕ), sInf ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P) ≤ φStar) (h_weak_duality : φStar ≤ fStar) (hδ_bddAbove : ∀ (N : ℕ), BddAbove ((fun (N : ℕ) => gapFunctionCertificate (y N) (α N) g) N '' P)) (hδ_le : ∀ (N : ℕ), sSup ((fun (N : ℕ) => gapFunctionCertificate (y N) (α N) g) N '' P) ≤ r N) (N : ℕ) : (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - fStar + (φStar - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N))) N ∈ Set.Icc 0 ((fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) N) ∧ (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) N ≤ r N

Companion sSup reformulation of Lemma 3.24. The source-facing statement above uses an explicit attained maximum δMax N; this theorem keeps only the canonical supremum bound.

theorem weightedPrimalDualGap_nonneg_le_of_gapFunctionCertificate_bound {E : Type u} {U : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [AddCommGroup U] [Module ℝ U] {P : Set E} {ψ : E → U → ℝ} {g : E → E} (y : (N : ℕ) → Fin (N + 1) → E) (u : (N : ℕ) → Fin (N + 1) → U) (α : (N : ℕ) → Fin (N + 1) → ℝ) (r : ℕ → ℝ) (hP_nonempty : P.Nonempty) (hlower_bddBelow : ∀ (N : ℕ), BddBelow ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P)) (hα_nonneg : ∀ (N : ℕ) (k : Fin (N + 1)), 0 ≤ α N k) (hα_sum_one : ∀ (N : ℕ), ∑ k : Fin (N + 1), α N k = 1) (hsubgradient_uHat : ∀ (N : ℕ) (k : Fin (N + 1)), ∀ x ∈ P, ψ (y N k) (Finset.univ.centerMass (α N) (u N)) - ψ x (Finset.univ.centerMass (α N) (u N)) ≤ inner ℝ (g (y N k)) (y N k - x)) (haggregate : ∀ (N : ℕ), (α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) ≤ ∑ k : Fin (N + 1), α N k * ψ (y N k) (Finset.univ.centerMass (α N) (u N))) (fStar φStar : ℝ) (h_primal_lower : ∀ (N : ℕ), fStar ≤ α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) (h_dual_upper_uHat : ∀ (N : ℕ), sInf ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P) ≤ φStar) (h_weak_duality : φStar ≤ fStar) (hdelta : ∀ (N : ℕ), ∀ x ∈ P, (fun (N : ℕ) => gapFunctionCertificate (y N) (α N) g) N x ≤ r N) (N : ℕ) : 0 ≤ (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) N ∧ (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) N ≤ r N

Companion gap-only corollary of Lemma 3.24 under pointwise certificate control.

theorem weightedPrimalDualGap_tendsto_zero_of_gapFunctionCertificate_bound {E : Type u} {U : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [AddCommGroup U] [Module ℝ U] {P : Set E} {ψ : E → U → ℝ} {g : E → E} (y : (N : ℕ) → Fin (N + 1) → E) (u : (N : ℕ) → Fin (N + 1) → U) (α : (N : ℕ) → Fin (N + 1) → ℝ) (r : ℕ → ℝ) (hP_nonempty : P.Nonempty) (hlower_bddBelow : ∀ (N : ℕ), BddBelow ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P)) (hα_nonneg : ∀ (N : ℕ) (k : Fin (N + 1)), 0 ≤ α N k) (hα_sum_one : ∀ (N : ℕ), ∑ k : Fin (N + 1), α N k = 1) (hsubgradient_uHat : ∀ (N : ℕ) (k : Fin (N + 1)), ∀ x ∈ P, ψ (y N k) (Finset.univ.centerMass (α N) (u N)) - ψ x (Finset.univ.centerMass (α N) (u N)) ≤ inner ℝ (g (y N k)) (y N k - x)) (haggregate : ∀ (N : ℕ), (α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) ≤ ∑ k : Fin (N + 1), α N k * ψ (y N k) (Finset.univ.centerMass (α N) (u N))) (fStar φStar : ℝ) (h_primal_lower : ∀ (N : ℕ), fStar ≤ α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) (h_dual_upper_uHat : ∀ (N : ℕ), sInf ((fun (x : E) => ψ x (Finset.univ.centerMass (α N) (u N))) '' P) ≤ φStar) (h_weak_duality : φStar ≤ fStar) (hdelta : ∀ (N : ℕ), ∀ x ∈ P, (fun (N : ℕ) => gapFunctionCertificate (y N) (α N) g) N x ≤ r N) (hr_tendsto : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (N : ℕ) => (fun (N : ℕ) => α N ⬝ᵥ fun (k : Fin (N + 1)) => ψ (y N k) (u N k)) N - (fun (u' : U) => sInf ((fun (x : E) => ψ x u') '' P)) ((fun (N : ℕ) => Finset.univ.centerMass (α N) (u N)) N)) Filter.atTop (nhds 0)

Companion convergence form under pointwise certificate control.