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.
The moment system of admissible weight vectors. w ∈ MomentSol p β means that for every degree ℓ ≤ β the sampled weighted sum ∑ j, w j * (p j) ^ ℓ equals 1^ℓ - 0^ℓ, i.e. 0 when ℓ = 0 and 1 otherwise. Equivalently, w reproduces the endpoint contrast r ↦ r.eval 1 - r.eval 0 on every real polynomial r of degree ≤ β via the node values (r.eval (p j))ⱼ.
The set of achievable ℓ¹ norms of admissible weights: primalNormSet p β = { ∑ j, |w j| : w ∈ MomentSol p β }. Its infimum is the primal (min-norm-representation) value.
Definition (Lean source)
The set of achievable endpoint contrasts of node-bounded polynomials: dualValSet p β = { |r.eval 1 - r.eval 0| : r.natDegree ≤ β, ∀ j, |r.eval (p j)| ≤ 1 }. Its supremum is the dual value.
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.
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).conclusion(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.conclusionBddBelow (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.Proof (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.Proof (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.
The degree-≤ β polynomial ∑ i, b i * X^i associated to a coefficient vector b : Fin (β+1) → ℝ. Its node values are Ev p β b and its endpoint contrast is contrastL β b.
Definition (Lean source)
Node evaluation as a linear map: Ev p β b is the vector of values of the degree-≤ β polynomial with coefficients b, sampled at the nodes, (Ev p β b) j = ∑ i, b i * (p j)^i. This is the transpose of the moment map.
Definition (Lean source)
Endpoint-contrast functional on coefficient vectors: contrastL β b = ∑ i, b i * (if i = 0 then 0 else 1) = r.eval 1 - r.eval 0 for r = coeffPoly b.
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.
Proof (Lean source)
The sup norm maxⱼ |x j| on Fin (k+1) → ℝ (a Finset.sup' over the nonempty index set). Used as the majorant M · ninf in Hahn–Banach.
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.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] -
coeffPoly_eval_nodetheorem — Node values of coeffPoly b coincide with Ev p β b.Proof (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).hypothesesb :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.hypothesesb :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)^ℓ. -
contrastL_singletheorem — The contrast of the ℓ-th coordinate vector is 1^ℓ - 0^ℓ.hypothesesℓ :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.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.Proof (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.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.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.hypothesesProof (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).hypothesesconclusionProof (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.Proof (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.Proof (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).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⟩