Mathlib.Analysis.FiniteDimL1LinfDuality
Finite-dimensional l1-linfinity duality helpers: polynomial evaluation maps, moment systems, weak and strong duality, and Hahn-Banach setup.
Basic 4 core · 4 supporting Fix k + 1 nodes p : Fin (k+1) → ℝ and a degree bound β ≤ k. ★ momentSol_nonempty
Finite-dimensional ℓ¹/ℓ∞ duality for minimum-norm node representation — definitions
Fix k + 1 nodes p : Fin (k+1) → ℝ and a degree bound β ≤ k. We study the
minimum ℓ¹ norm of a weight vector w : Fin (k+1) → ℝ that reproduces the
endpoint contrast r ↦ r.eval 1 - r.eval 0 on every real polynomial r of
degree ≤ β, sampled at the nodes.
The weight w reproduces the contrast on all degree-≤ β polynomials iff it
solves the moment system
∑ j, w j * (p j) ^ ℓ = (if ℓ = 0 then 0 else 1) for every ℓ ≤ β
(test against monomials X^ℓ; the RHS is 1^ℓ - 0^ℓ). That system is the set
MomentSol p β.
The two extremal quantities are
* the primal sInf (primalNormSet p β) — the least achievable ∑ j, |w j|
over w ∈ MomentSol p β;
* the dual sSup (dualValSet p β) — the largest achievable
|r.eval 1 - r.eval 0| over polynomials r of degree ≤ β bounded by 1 at
the nodes.
The main theorem l1_repr_eq_sup_dual (in Duality.lean) is the identity
sInf (primalNormSet p β) = sSup (dualValSet p β): finite-dimensional
ℓ¹/ℓ∞ Hahn–Banach / LP duality specialised to the node-sampling map.
This file only sets up the definitions and the basic well-posedness facts
(nonemptiness / boundedness of the two real sets). Everything is stated for
arbitrary distinct nodes and arbitrary β ≤ k, so it is reusable and not
gerrymandered to any downstream schedule.
## Standard reference
Finite-dimensional LP duality / ℓ¹–ℓ∞ Hahn–Banach duality (the ℓ¹/ℓ∞ pairing on
ℝⁿ); the min-norm-representation = dual-sup identity is standard
optimal-recovery / convex-analysis duality.
For a nonnegative number of nodes minus one, a collection of real nodes indexed from zero through that number, and a nonnegative degree bound, the moment system of admissible weight vectors consists of precisely those real weight vectors whose weighted power sum at every nonnegative degree no greater than the bound is zero at degree zero and one at every positive degree.
For a nonnegative number of nodes minus one, a collection of real nodes indexed from zero through that number, and a nonnegative degree bound, the set of achievable primal norms consists of the sums of absolute weights over all weight vectors that satisfy the corresponding moment system.
For a nonnegative number of nodes minus one, a collection of real nodes indexed from zero through that number, and a nonnegative degree bound, the set of achievable dual values consists of the absolute differences between a real polynomial's values at one and zero, for every polynomial of degree at most the bound whose absolute value at every node is at most one.
Definition (Lean source)
Feasibility of the moment system (Vandermonde). For k + 1 pairwise distinct real interpolation nodes and a degree bound β at most k, the moment system — the set of weight vectors that reproduce the endpoint contrast of every degree-≤ β polynomial through the node values — has a solution.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
dualValSet_nonemptytheorem — The dual set is nonempty: the zero polynomial contributes the value 0 (degree 0 ≤ β, trivially node-bounded, contrast 0).hypothesesconclusion(dualValSet p β).NonemptyProof (Lean source)
theorem dualValSet_nonempty : (dualValSet p β).Nonempty := by refine ⟨0, ?_⟩ refine ⟨(0 : Polynomial ℝ), ?_, ?_, ?_⟩ · simp · intro j simp · simp -
primalNormSet_bddBelowtheorem — Every element of the primal set is ≥ 0 (a sum of absolute values), so the set is bounded below by 0.hypothesesconclusionBddBelow (primalNormSet p β)Proof (Lean source)
theorem primalNormSet_bddBelow : BddBelow (primalNormSet p β) := by refine ⟨0, fun s hs => ?_⟩ rcases hs with ⟨w, _hw, rfl⟩ exact sum_nonneg (fun j _ => abs_nonneg (w j)) -
primalNormSet_nonnegtheorem — 0 is a lower bound for the primal set.hypothesesconclusion0 ≤ sProof (Lean source)
theorem primalNormSet_nonneg {s : ℝ} (hs : s ∈ primalNormSet p β) : 0 ≤ s := by rcases hs with ⟨w, _hw, rfl⟩ exact sum_nonneg (fun j _ => abs_nonneg (w j)) -
primalNormSet_nonemptytheorem — The primal set is nonempty whenever the moment system is solvable.hypothesesconclusion(primalNormSet p β).NonemptyProof (Lean source)
theorem primalNormSet_nonempty (hp : Injective p) (hβ : β ≤ k) : (primalNormSet p β).Nonempty := by rcases momentSol_nonempty (p := p) hp hβ with ⟨w, hw⟩ exact ⟨∑ j, |w j|, w, hw, rfl⟩
HahnBanachSetup 6 core · 14 supporting The hard (primal ≤ dual) direction is proved with the *sublinear* Hahn–Banach theorem exists_extension_of_le_sublinear, which works on a plain real vector space (Fin (k+1) → ℝ) and needs no normed-space / PiLp / operator ★ Ev_injective★ contrastL_le_dual_mul_ninf
Setup for strong duality: the algebraic Hahn–Banach route
The hard (primal ≤ dual) direction is proved with the sublinear Hahn–Banach
theorem exists_extension_of_le_sublinear, which works on a plain real vector
space (Fin (k+1) → ℝ) and needs no normed-space / PiLp / operator-norm
development. This file collects the algebraic objects it consumes:
* coeffPoly b — the degree-≤ β polynomial ∑ i, b i * X^i with coefficient
vector b : Fin (β+1) → ℝ;
* Ev p β : (Fin (β+1) → ℝ) →ₗ[ℝ] (Fin (k+1) → ℝ) — node evaluation
b ↦ (∑ i, b i * (p j)^i)_j (the transpose of the moment map);
* contrastL β : (Fin (β+1) → ℝ) →ₗ[ℝ] ℝ — the endpoint contrast
b ↦ ∑ i, b i * (1^i - 0^i) of the coefficient vector;
* ninf x — the sup norm maxⱼ |x j| on Fin (k+1) → ℝ;
* Ev_injective — node evaluation is injective for distinct nodes and β ≤ k
(Vandermonde), so the contrast is a well-defined linear functional on the
node-value subspace range (Ev p β);
* contrastL_le_dual_mul_ninf — the boundedness estimate
contrastL β b ≤ (sSup (dualValSet p β)) * ninf (Ev p β b), i.e. the contrast
functional is dominated by M · ‖·‖_∞ on the subspace, which is exactly the
hypothesis of the sublinear Hahn–Banach theorem.
StrongDuality.lean assembles these into the extension g, reads off the ℓ¹
representing vector w j = g (Pi.single j 1), and derives admissibility and the
norm bound.
For a nonnegative degree bound and a real coefficient vector indexed from zero through that bound, the associated coefficient polynomial is the sum of each coefficient times the corresponding monomial. Its degree is at most the stated bound.
Definition (Lean source)
For a nonnegative number of sampled coordinates minus one, a collection of real sampling nodes indexed from zero through that number, and a nonnegative degree bound, the node-evaluation linear map sends a coefficient vector to the values at all sampling nodes of its polynomial of degree at most that bound.
Definition (Lean source)
For a nonnegative degree bound, the endpoint-contrast linear functional maps a coefficient vector to the value at one minus the value at zero of its associated polynomial.
Definition (Lean source)
Node evaluation is injective. For k + 1 pairwise distinct real nodes and a degree bound β at most k, the linear map sending a degree-≤ β coefficient vector to its values at the nodes is injective.
Formal statement
Proof (Lean source)
For a nonnegative number of coordinates minus one and a real vector indexed from zero through that number, the sup norm is the largest absolute coordinate value.
Definition (Lean source)
Boundedness estimate (the Hahn–Banach hypothesis). For k + 1 pairwise distinct real nodes, a degree bound β at most k, and any coefficient vector b, the endpoint-contrast functional evaluated at b is bounded above by the dual supremum times the sup-norm of b's node values.
Formal statement
Proof (Lean source)
14 supporting declarations (lemmas, instances)
-
coeffPoly_natDegree_letheorem — coeffPoly b has degree at most β (each monomial X^i has i ≤ β).Proof (Lean source)
theorem coeffPoly_natDegree_le (b : Fin (β + 1) → ℝ) : (coeffPoly b).natDegree ≤ β := by rw [coeffPoly] refine Polynomial.natDegree_sum_le_of_forall_le (s := univ) (f := fun i : Fin (β + 1) => Polynomial.C (b i) * Polynomial.X ^ (i : ℕ)) ?_ intro i hi exact (Polynomial.natDegree_C_mul_X_pow_le (b i) (i : ℕ)).trans (Nat.le_of_lt_succ i.isLt) -
coeffPoly_evaltheorem — Evaluating coeffPoly b at t gives the polynomial value ∑ i, b i * t^i.hypothesesconclusion(coeffPoly b).eval t = ∑ i, b i * t ^ (i : ℕ)Proof (Lean source)
theorem coeffPoly_eval (b : Fin (β + 1) → ℝ) (t : ℝ) : (coeffPoly b).eval t = ∑ i, b i * t ^ (i : ℕ) := by rw [coeffPoly, Polynomial.eval_finset_sum] simp only [Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow, Polynomial.eval_X] -
Ev_applytheorem — Unfolding lemma for Ev (definitional).hypothesesconclusionEv p β b j = ∑ i, b i * p j ^ (i : ℕ) -
coeffPoly_eval_nodetheorem — Node values of coeffPoly b coincide with Ev p β b.hypothesesProof (Lean source)
theorem coeffPoly_eval_node (b : Fin (β + 1) → ℝ) (j : Fin (k + 1)) : (coeffPoly b).eval (p j) = Ev p β b j := by rw [coeffPoly_eval, Ev_apply] -
contrastL_applytheorem — Unfolding lemma for contrastL (definitional).hypothesesβ :sharedℕb :Fin (β + 1) → ℝconclusioncontrastL β b = ∑ i, b i * (if (i : ℕ) = 0 then (0 : ℝ) else 1)Proof (Lean source)
theorem contrastL_apply (b : Fin (β + 1) → ℝ) : contrastL β b = ∑ i, b i * (if (i : ℕ) = 0 then (0 : ℝ) else 1) := by rfl -
coeffPoly_contrasttheorem — The contrast functional computes the endpoint contrast of coeffPoly b.hypothesesβ :sharedℕb :Fin (β + 1) → ℝProof (Lean source)
theorem coeffPoly_contrast (b : Fin (β + 1) → ℝ) : (coeffPoly b).eval 1 - (coeffPoly b).eval 0 = contrastL β b := by rw [coeffPoly_eval, coeffPoly_eval, contrastL_apply] rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl ?_ intro i hi by_cases h : (i : ℕ) = 0 · simp [h] · simp [h] -
Ev_singletheorem — Node evaluation of the ℓ-th coordinate vector recovers the monomial column (p j)^ℓ.hypotheses -
contrastL_singletheorem — The contrast of the ℓ-th coordinate vector is 1^ℓ - 0^ℓ.hypothesesβ :sharedℕℓ :Fin (β + 1)Proof (Lean source)
theorem contrastL_single (ℓ : Fin (β + 1)) : contrastL β (single ℓ (1 : ℝ)) = if (ℓ : ℕ) = 0 then (0 : ℝ) else 1 := by rw [contrastL_apply] rw [Finset.sum_eq_single ℓ] · simp · intro i hi hne simp [Pi.single_eq_of_ne hne] · intro h exact (h (Finset.mem_univ ℓ)).elim -
le_ninftheorem — Each coordinate is bounded by the sup norm: |x j| ≤ ninf x. -
ninf_nonnegtheorem — The sup norm is nonnegative.Proof (Lean source)
theorem ninf_nonneg (x : Fin (k + 1) → ℝ) : 0 ≤ ninf x := by exact (abs_nonneg (x 0)).trans (le_ninf x 0) -
ninf_smultheorem — Positive homogeneity (with absolute value) of the sup norm.Proof (Lean source)
theorem ninf_smul (c : ℝ) (x : Fin (k + 1) → ℝ) : ninf (c • x) = |c| * ninf x := by apply le_antisymm · rw [ninf] apply Finset.sup'_le intro j hj calc |c • x j| = |c| * |x j| := by simp [smul_eq_mul, abs_mul] _ ≤ |c| * ninf x := mul_le_mul_of_nonneg_left (le_ninf x j) (abs_nonneg c) · obtain ⟨j, hj, hsup⟩ := Finset.exists_mem_eq_sup' (s := univ) (H := ⟨0, Finset.mem_univ 0⟩) (f := fun j => |x j|) change |c| * (Finset.univ.sup' ⟨0, Finset.mem_univ 0⟩ fun j => |x j|) ≤ ninf (c • x) rw [hsup] calc |c| * |x j| = |(c • x) j| := by simp [smul_eq_mul, abs_mul] _ ≤ ninf (c • x) := le_ninf (c • x) j -
ninf_add_letheorem — Subadditivity (triangle inequality) of the sup norm. -
ninf_signtheorem — The sup norm of a ±1 sign vector is 1. -
dual_nonnegtheorem — Dual value is nonnegative. 0 ∈ dualValSet p β (the zero polynomial) and the set is bounded above, so its supremum is ≥ 0.hypothesesconclusion0 ≤ sSup (dualValSet p β)Proof (Lean source)
theorem dual_nonneg (hbounded : BddAbove (dualValSet p β)) : 0 ≤ sSup (dualValSet p β) := by have h0 : 0 ∈ dualValSet p β := by refine ⟨(0 : Polynomial ℝ), ?_, ?_, ?_⟩ · simp · intro j simp · simp exact le_csSup hbounded h0
Duality 2 core · 0 supporting Assembles weak duality (sSup_dual_le_sInf_primal) and strong duality (sInf_primal_le_sSup_dual) into the min-norm-representation = dual-sup identity for the node-sampling map, plus the squared corollary used downstream. ★ l1_repr_eq_sup_dual★ l1_repr_sq_eq_sup_dual_sq
Finite-dimensional ℓ¹/ℓ∞ duality — the main identity
Assembles weak duality (sSup_dual_le_sInf_primal) and strong duality
(sInf_primal_le_sSup_dual) into the min-norm-representation = dual-sup
identity for the node-sampling map, plus the squared corollary used downstream.
Finite-dimensional ℓ¹/ℓ∞ duality. For k + 1 pairwise distinct real interpolation nodes and a degree bound β at most k, the least ℓ¹ norm of a weight vector that reproduces the endpoint contrast r ↦ r.eval 1 - r.eval 0 of every degree-≤ β polynomial through its node values equals the largest such contrast attained by a degree-≤ β polynomial bounded by 1 at every node.
Formal statement
Proof (Lean source)
Squared form. Under the same hypotheses as l1_repr_eq_sup_dual — k + 1 pairwise distinct real interpolation nodes and a degree bound β at most k — the square of the min-norm-representation value equals the square of the dual sup.
Formal statement
Proof (Lean source)
NonemptyDuality 2 core · 7 supporting The generic theorem l1_repr_eq_sup_dual assumes distinct nodes and β ≤ k to get injectivity of the node-evaluation map and hence feasibility of the moment system. ★ exists_moment_le_dual_of_momentSol_nonempty★ l1_repr_eq_sup_dual_of_momentSol_nonempty
Finite-dimensional ℓ¹/ℓ∞ duality from moment-system feasibility
The generic theorem l1_repr_eq_sup_dual assumes distinct nodes and β ≤ k to
get injectivity of the node-evaluation map and hence feasibility of the moment
system. Downstream formalizations sometimes already carry feasibility as a
hypothesis. This file packages the same Hahn-Banach proof under the weaker and
more intrinsic assumption (MomentSol p β).Nonempty.
Main declarations:
* primalNormSet_nonempty_of_momentSol_nonempty and
dualValSet_bddAbove_of_momentSol_nonempty establish that the primal infimum
and dual supremum are well posed from feasibility alone.
* momentSol_contrast_eq_sum_eval identifies a feasible moment vector with a
representation of the coefficient contrast on node-value vectors.
* contrastL_le_dual_mul_ninf_of_momentSol_nonempty is the Hahn-Banach
domination estimate without a Vandermonde injectivity assumption.
* exists_moment_le_dual_of_momentSol_nonempty produces a feasible weight with
ℓ¹ norm bounded by the dual value.
* l1_repr_eq_sup_dual_of_momentSol_nonempty is the resulting ℓ¹/ℓ∞ duality
identity assuming only moment-system feasibility.
Strong duality from moment-system feasibility. If the moment system for the given nodes and degree bound is feasible, i.e. it has at least one solution, then there exists a feasible weight vector whose ℓ¹ norm is at most the dual supremum.
Formal statement
Proof (Lean source)
Finite-dimensional ℓ¹/ℓ∞ duality under feasibility alone. If the moment system for the given nodes and degree bound has at least one solution, then the least ℓ¹ norm among feasible weight vectors equals the largest endpoint contrast attained by a degree-bounded polynomial bounded by 1 at every node.
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
primalNormSet_nonempty_of_momentSol_nonemptytheorem — If the moment system is feasible, the primal norm set is nonempty.hypothesesconclusion(primalNormSet p β).NonemptyProof (Lean source)
theorem primalNormSet_nonempty_of_momentSol_nonempty (hne : (MomentSol p β).Nonempty) : (primalNormSet p β).Nonempty := by rcases hne with ⟨w, hw⟩ exact ⟨∑ j, |w j|, w, hw, rfl⟩ -
dualValSet_bddAbove_of_momentSol_nonemptytheorem — Feasibility of the moment system bounds every dual value by any feasible primal norm. This is the weak-duality estimate: if w ∈ MomentSol p β, then every node-bounded degree-≤ β polynomial has endpoint contrast at most ∑ j, |w j|, so the dual value set is bounded above.hypothesesconclusionBddAbove (dualValSet p β)Proof (Lean source)
theorem dualValSet_bddAbove_of_momentSol_nonempty (hne : (MomentSol p β).Nonempty) : BddAbove (dualValSet p β) := by rcases primalNormSet_nonempty_of_momentSol_nonempty (p := p) (β := β) hne with ⟨s, hs⟩ exact ⟨s, fun t ht => dual_le_primal hs ht⟩ -
dual_nonneg_of_momentSol_nonemptytheorem — With a feasible primal system, the dual supremum is nonnegative because 0 is dual-feasible.hypothesesconclusion0 ≤ sSup (dualValSet p β)Proof (Lean source)
theorem dual_nonneg_of_momentSol_nonempty (hne : (MomentSol p β).Nonempty) : 0 ≤ sSup (dualValSet p β) := by have h0 : 0 ∈ dualValSet p β := by refine ⟨(0 : Polynomial ℝ), ?_, ?_, ?_⟩ · simp · intro j simp · simp exact le_csSup (dualValSet_bddAbove_of_momentSol_nonempty (p := p) (β := β) hne) h0 -
momentSol_contrast_eq_sum_evaltheorem — A feasible moment vector represents the coefficient contrast on node-value vectors: for every coefficient vector b, contrastL β b equals the pairing of w with the node-evaluation vector Ev p β b.Proof (Lean source)
theorem momentSol_contrast_eq_sum_eval {w : Fin (k + 1) → ℝ} (hw : w ∈ MomentSol p β) (b : Fin (β + 1) → ℝ) : contrastL β b = ∑ j, w j * Ev p β b j := by have hrepr := repr_identity (p := p) (β := β) (w := w) hw (coeffPoly_natDegree_le b) rw [coeffPoly_contrast] at hrepr rw [hrepr] refine Finset.sum_congr rfl ?_ intro j _ rw [← coeffPoly_eval_node (p := p) b j] -
contrastL_le_dual_mul_ninf_of_momentSol_nonemptytheorem — Hahn-Banach domination estimate on the node-value subspace, using feasibility instead of node-evaluation injectivity: contrastL β b ≤ sSup (dualValSet p β) * ninf (Ev p β b).Proof (Lean source)
theorem contrastL_le_dual_mul_ninf_of_momentSol_nonempty (hne : (MomentSol p β).Nonempty) (b : Fin (β + 1) → ℝ) : contrastL β b ≤ sSup (dualValSet p β) * ninf (Ev p β b) := by rcases hne with ⟨w0, hw0⟩ let M := sSup (dualValSet p β) let s := ninf (Ev p β b) by_cases hs0 : s = 0 · have hEvzero : Ev p β b = 0 := by ext j have hle : |Ev p β b j| ≤ 0 := by simpa [s, hs0] using le_ninf (Ev p β b) j exact abs_eq_zero.mp (le_antisymm hle (abs_nonneg (Ev p β b j))) have hcontrast_zero : contrastL β b = 0 := by rw [momentSol_contrast_eq_sum_eval (p := p) (β := β) hw0 b] simp [hEvzero] simp only [hcontrast_zero] exact mul_nonneg (dual_nonneg_of_momentSol_nonempty (p := p) (β := β) ⟨w0, hw0⟩) (by simp [s, hs0]) · have hspos : 0 < s := lt_of_le_of_ne (by simpa [s] using ninf_nonneg (Ev p β b)) (Ne.symm hs0) let r' : Polynomial ℝ := s⁻¹ • coeffPoly b have hmem : |r'.eval 1 - r'.eval 0| ∈ dualValSet p β := by refine ⟨r', ?_, ?_, rfl⟩ · exact (Polynomial.natDegree_smul_le s⁻¹ (coeffPoly b)).trans (coeffPoly_natDegree_le b) · intro j have hle : |Ev p β b j| ≤ s := by simpa [s] using le_ninf (Ev p β b) j calc |r'.eval (p j)| = |s⁻¹ * Ev p β b j| := by rw [show r'.eval (p j) = s⁻¹ * Ev p β b j by simp [r', Polynomial.eval_smul, coeffPoly_eval_node]] _ = s⁻¹ * |Ev p β b j| := by rw [abs_mul, abs_inv, abs_of_pos hspos] _ ≤ s⁻¹ * s := mul_le_mul_of_nonneg_left hle (inv_nonneg.mpr hspos.le) _ = 1 := inv_mul_cancel₀ hspos.ne' have hdual : |r'.eval 1 - r'.eval 0| ≤ M := by exact le_csSup (dualValSet_bddAbove_of_momentSol_nonempty (p := p) (β := β) ⟨w0, hw0⟩) hmem have hscaled : r'.eval 1 - r'.eval 0 = s⁻¹ * contrastL β b := by calc r'.eval 1 - r'.eval 0 = s⁻¹ * (coeffPoly b).eval 1 - s⁻¹ * (coeffPoly b).eval 0 := by simp [r', Polynomial.eval_smul] _ = s⁻¹ * ((coeffPoly b).eval 1 - (coeffPoly b).eval 0) := by ring _ = s⁻¹ * contrastL β b := by rw [coeffPoly_contrast] have habs_le : |contrastL β b| ≤ M * s := by calc |contrastL β b| = s * |s⁻¹ * contrastL β b| := by rw [abs_mul, abs_inv, abs_of_pos hspos, ← mul_assoc, mul_inv_cancel₀ hspos.ne', one_mul] _ ≤ s * M := mul_le_mul_of_nonneg_left (by simpa [hscaled] using hdual) hspos.le _ = M * s := by rw [mul_comm] exact (le_abs_self (contrastL β b)).trans (by simpa [M, s] using habs_le) -
sInf_primal_le_sSup_dual_of_momentSol_nonemptytheorem — Inequality form of strong duality under moment-system feasibility.hypothesesconclusionProof (Lean source)
theorem sInf_primal_le_sSup_dual_of_momentSol_nonempty (hne : (MomentSol p β).Nonempty) : sInf (primalNormSet p β) ≤ sSup (dualValSet p β) := by obtain ⟨w, hw, hw_norm⟩ := exists_moment_le_dual_of_momentSol_nonempty (p := p) (β := β) hne exact le_trans (csInf_le primalNormSet_bddBelow ⟨w, hw, rfl⟩) hw_norm -
sSup_dual_le_sInf_primal_of_momentSol_nonemptytheorem — Weak duality as an sSup ≤ sInf inequality under moment-system feasibility.hypothesesconclusionProof (Lean source)
theorem sSup_dual_le_sInf_primal_of_momentSol_nonempty (hne : (MomentSol p β).Nonempty) : sSup (dualValSet p β) ≤ sInf (primalNormSet p β) := by exact csSup_le dualValSet_nonempty fun t ht => le_csInf (primalNormSet_nonempty_of_momentSol_nonempty (p := p) (β := β) hne) fun s hs => dual_le_primal hs ht
StrongDuality 2 core · 0 supporting This file specializes the feasibility-based finite-dimensional ℓ¹/ℓ∞ duality API to distinct nodes with degree bound β ≤ k. ★ exists_moment_le_dual★ sInf_primal_le_sSup_dual
Strong duality from distinct interpolation nodes
This file specializes the feasibility-based finite-dimensional ℓ¹/ℓ∞ duality
API to distinct nodes with degree bound β ≤ k. Vandermonde feasibility is
provided by momentSol_nonempty, while the Hahn–Banach certificate is supplied
by exists_moment_le_dual_of_momentSol_nonempty.
Strong duality (existence of an optimal weight). For k + 1 pairwise distinct real nodes and a degree bound β at most k, there exists a feasible weight vector — one solving the moment system — whose ℓ¹ norm does not exceed the dual supremum.
Formal statement
Proof (Lean source)
Strong duality (inequality form). For k + 1 pairwise distinct real nodes and a degree bound β at most k, the least ℓ¹ norm among feasible weight vectors is at most the dual supremum.
Formal statement
Proof (Lean source)
WeakDuality 3 core · 1 supporting The analytic core is the representation identity: an admissible weight w reproduces the endpoint contrast of every degree-≤ β polynomial through its node values, r.eval 1 - r.eval 0 = ∑ j, w j * r.eval (p j). ★ repr_identity★ dual_le_primal★ sSup_dual_le_sInf_primal
Weak duality: the representation identity and dual ≤ primal
The analytic core is the representation identity: an admissible weight w
reproduces the endpoint contrast of every degree-≤ β polynomial through its
node values,
r.eval 1 - r.eval 0 = ∑ j, w j * r.eval (p j).
From it, weak duality is immediate:
`|r.eval 1 - r.eval 0| = |∑ j, w j * r.eval (p j)| ≤ ∑ j, |w j| * |r.eval (p j)|
≤ ∑ j, |w j|`
whenever |r.eval (p j)| ≤ 1 at every node. Thus every dual value is ≤ every
primal value, i.e. dual_le_primal, giving sSup (dualValSet) ≤ sInf (primalNormSet).
Representation identity. If a weight vector solves the moment system for the given nodes and degree bound and a real polynomial has degree at most β, then the polynomial's endpoint contrast, r.eval 1 - r.eval 0, is reproduced exactly by the weighted sum of its values at the nodes.
Formal statement
Proof (Lean source)
Weak duality. If a real number is the ℓ¹ norm of some feasible weight vector and another real number is the endpoint contrast attained by some node-bounded degree-≤ β polynomial, then the second number is no larger than the first: every dual value is bounded by every primal value.
Formal statement
Proof (Lean source)
Weak duality (inequality form). If the primal set of achievable ℓ¹ norms is nonempty, then the dual supremum is at most the primal infimum: every dual value is bounded by every primal value, hence so is the supremum of dual values by the infimum of primal values.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
dualValSet_bddAbovetheorem — The dual set is bounded above (by any primal value; the primal set is nonempty for distinct nodes and β ≤ k).hypothesesconclusionBddAbove (dualValSet p β)Proof (Lean source)
theorem dualValSet_bddAbove (hne : (primalNormSet p β).Nonempty) : BddAbove (dualValSet p β) := by rcases hne with ⟨s, hs⟩ exact ⟨s, fun t ht => dual_le_primal hs ht⟩