The quadratic module of a set of relations, Archimedean separation, and the ℓ¹ norm

Fix a set R of noncommutative polynomials in letters G (MIPRE.NCPoly G), the relations. The Tsirelson route (planning/tsirelson-campaign.md, §3.1) works with one object, the quadratic module M = qmod R := PointedCone.hull ℝ ({s⋆ g s : g ∈ {1} ∪ G} ∪ relSpan R ∪ Anti), where relSpan R is the complex span of the u ρ v with ρ ∈ R (the two-sided ideal of the relations) and Anti is the real subspace of anti-hermitian elements z⋆ = -z. The letters are positive (g = 1⋆ g 1 ∈ M), and M is closed under m ↦ a⋆ m a (NCPoly.star_mul_mul_mem_qmod_of_mem).

Positivity. If the letters are evaluated at positive operators f g on a complex Hilbert space and the evaluation kills every relation, then every element of M has nonnegative expectation in every vector: 0 ≤ Re ⟪ψ, eval f m ψ⟫ (NCPoly.re_inner_eval_nonneg). The hermitian squares are positive, the ideal evaluates to 0, and anti-hermitian operators have purely imaginary expectations.

Archimedean property. If 1 - g² ∈ M for every letter, then every polynomial is bounded by a multiple of the unit: ∀ y, ∃ N, N • 1 + y ∈ M (NCPoly.archimedean_of_gen). The proof telescopes 1 - w⋆ w ∈ M along a word (NCPoly.one_sub_star_word_mem), writes a monomial c w = α w + (α w)⋆ + (α w - (α w)⋆) with α = c/2, and uses (1 + |α|²)·1 + α w + (α w)⋆ = (1 + α w)⋆ (1 + α w) + |α|² (1 - w⋆ w) (NCPoly.herm_add_const_mem); the anti-hermitian remainder lies in Anti. For a letter with 1 - g ∈ M, 1 - g² ∈ M follows from g - g² = g (1 - g) g + (1 - g) g (1 - g) (NCPoly.one_sub_gen_sq_mem).

Separation. In any real vector space, a pointed cone M for which u is an order unit (∀ y, ∃ N, N • u + y ∈ M) and which misses -u carries a nonnegative linear functional with L u = 1 (MIPRE.exists_nonneg_functional_of_archimedean, from Mathlib's riesz_extension). If moreover u ∈ M and h ∉ M, the functional can be chosen with L h ≤ 0 (MIPRE.exists_separating_functional_of_archimedean), by applying the first statement to M ⊔ hull {-h}. This is the separation step of the Positivstellensatz (§3.4). The two statements hold in any real vector space, and live in the namespace MIPRE rather than MIPRE.PointedCone, which would shadow Mathlib's PointedCone inside namespace MIPRE.

The ℓ¹ norm. The exact certificates of §3.5 round a real certificate coefficientwise, and measure the error in the taxicab ℓ¹ norm ‖z‖₁ = Σ_w (|Re z_w| + |Im z_w|) (NCPoly.l1). It is subadditive, submultiplicative, invariant under negation and the star, and bounded on complex multiples by the taxicab norm of the scalar, so no topology on NCPoly G is needed.

Main declarations

• NCPoly.relSpan R, NCPoly.sosGens, NCPoly.qmod R, and the membership lemmas;
• NCPoly.mul_mem_relSpan, NCPoly.star_mul_mul_mem_qmod_of_mem;
• NCPoly.eval_eq_zero_of_mem_relSpan, NCPoly.re_inner_eq_zero_of_star_eq_neg, NCPoly.re_inner_eval_nonneg;
• NCPoly.one_sub_gen_sq_mem, NCPoly.one_sub_star_word_mem, NCPoly.herm_add_const_mem, NCPoly.archimedean_of_gen;
• NCPoly.l1, with NCPoly.l1_nonneg, NCPoly.l1_zero, NCPoly.l1_single, NCPoly.l1_add_le, NCPoly.l1_neg, NCPoly.l1_smul_le, NCPoly.l1_sum_le, NCPoly.l1_star, NCPoly.l1_mul_le;
• MIPRE.exists_nonneg_functional_of_archimedean, MIPRE.exists_separating_functional_of_archimedean.

The relation span and the quadratic module

noncomputable def MIPRE.NCPoly.relSpan {G : Type u_1} (R : Set (NCPoly G)) : Submodule ℂ (NCPoly G)

The two-sided ideal generated by the relations R: the complex span of the products u * ρ * v with ρ ∈ R.

Equations

• MIPRE.NCPoly.relSpan R = Submodule.span ℂ {z : MIPRE.NCPoly G | ∃ (u : MIPRE.NCPoly G) (ρ : MIPRE.NCPoly G) (v : MIPRE.NCPoly G), ρ ∈ R ∧ z = u * ρ * v}

def MIPRE.NCPoly.sosGens (G : Type u_1) : Set (NCPoly G)

The hermitian squares s⋆ g s, with g either 1 (encoded as none) or a letter.

Equations

• MIPRE.NCPoly.sosGens G = {z : MIPRE.NCPoly G | ∃ (s : MIPRE.NCPoly G) (g : Option G), z = star s * g.elim 1 MIPRE.NCPoly.gen * s}

noncomputable def MIPRE.NCPoly.qmod {G : Type u_1} (R : Set (NCPoly G)) : PointedCone ℝ (NCPoly G)

The quadratic module M of the relations R: the real pointed cone generated by the hermitian squares s⋆ s and s⋆ g s, the relation ideal relSpan R, and the anti-hermitian elements.

Equations

• MIPRE.NCPoly.qmod R = PointedCone.hull ℝ (MIPRE.NCPoly.sosGens G ∪ ↑(MIPRE.NCPoly.relSpan R) ∪ ↑(skewAdjoint.submodule ℝ (MIPRE.NCPoly G)))

theorem MIPRE.NCPoly.mem_relSpan_of_mem {G : Type u_1} {R : Set (NCPoly G)} {ρ : NCPoly G} (h : ρ ∈ R) : ρ ∈ relSpan R

Every relation lies in the relation ideal.

theorem MIPRE.NCPoly.mul_mem_relSpan {G : Type u_1} {R : Set (NCPoly G)} {z : NCPoly G} (hz : z ∈ relSpan R) (a b : NCPoly G) : a * z * b ∈ relSpan R

The relation span is a two-sided ideal.

theorem MIPRE.NCPoly.one_mem_qmod {G : Type u_1} {R : Set (NCPoly G)} : 1 ∈ qmod R

The unit lies in the quadratic module.

theorem MIPRE.NCPoly.star_mul_mul_mem_qmod {G : Type u_1} {R : Set (NCPoly G)} (s : NCPoly G) (g : G) : star s * gen g * s ∈ qmod R

The hermitian square s⋆ g s of a letter lies in the quadratic module.

theorem MIPRE.NCPoly.star_mul_self_mem_qmod {G : Type u_1} {R : Set (NCPoly G)} (s : NCPoly G) : star s * s ∈ qmod R

The hermitian square s⋆ s lies in the quadratic module.

theorem MIPRE.NCPoly.gen_mem_qmod {G : Type u_1} {R : Set (NCPoly G)} (g : G) : gen g ∈ qmod R

Every letter lies in the quadratic module.

theorem MIPRE.NCPoly.mem_qmod_of_mem_relSpan {G : Type u_1} {R : Set (NCPoly G)} {z : NCPoly G} (hz : z ∈ relSpan R) : z ∈ qmod R

The relation ideal is contained in the quadratic module.

theorem MIPRE.NCPoly.mem_qmod_of_star_eq_neg {G : Type u_1} {R : Set (NCPoly G)} {z : NCPoly G} (hz : star z = -z) : z ∈ qmod R

Every anti-hermitian element lies in the quadratic module.

theorem MIPRE.NCPoly.star_mul_mul_mem_qmod_of_mem {G : Type u_1} {R : Set (NCPoly G)} {m : NCPoly G} (hm : m ∈ qmod R) (a : NCPoly G) : star a * m * a ∈ qmod R

The quadratic module is closed under m ↦ a⋆ m a.

Positivity under Hilbert-space evaluation

theorem MIPRE.NCPoly.eval_eq_zero_of_mem_relSpan {G : Type u_1} {R : Set (NCPoly G)} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (f : G → H →L[ℂ] H) (hR : ∀ ρ ∈ R, (eval f) ρ = 0) {z : NCPoly G} (hz : z ∈ relSpan R) : (eval f) z = 0

An evaluation that kills the relations kills the relation ideal.

theorem MIPRE.NCPoly.re_inner_eq_zero_of_star_eq_neg {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →L[ℂ] H) (hT : star T = -T) (ψ : H) : (inner ℂ ψ (T ψ)).re = 0

An anti-self-adjoint operator has purely imaginary expectations.

theorem MIPRE.NCPoly.re_inner_eval_nonneg {G : Type u_1} {R : Set (NCPoly G)} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : G → H →L[ℂ] H) (hf : ∀ (g : G), (f g).IsPositive) (hR : ∀ ρ ∈ R, (eval f) ρ = 0) (ψ : H) {m : NCPoly G} (hm : m ∈ qmod R) : 0 ≤ (inner ℂ ψ (((eval f) m) ψ)).re

Positivity of the quadratic module. Under an evaluation of the letters at positive operators that kills the relations, every element of qmod R has nonnegative expectation in every vector.

The Archimedean property

theorem MIPRE.NCPoly.one_sub_gen_sq_mem {G : Type u_1} {R : Set (NCPoly G)} {g : G} (hg : 1 - gen g ∈ qmod R) : 1 - gen g * gen g ∈ qmod R

If 1 - g ∈ M for a letter g, then 1 - g² ∈ M: add g - g² = g⋆ (1 - g) g + (1 - g)⋆ g (1 - g) to 1 - g.

theorem MIPRE.NCPoly.one_sub_star_word_mem {G : Type u_1} {R : Set (NCPoly G)} (hgen : ∀ (g : G), 1 - gen g * gen g ∈ qmod R) (w : FreeMonoid G) : 1 - star (single w 1) * single w 1 ∈ qmod R

If 1 - g² ∈ M for every letter, then 1 - w⋆ w ∈ M for every word w, by telescoping: 1 - (g w)⋆ (g w) = (1 - w⋆ w) + w⋆ (1 - g²) w.

theorem MIPRE.NCPoly.herm_add_const_mem {G : Type u_1} {R : Set (NCPoly G)} {s : NCPoly G} (hs : 1 - star s * s ∈ qmod R) (α : ℂ) : (1 + Complex.normSq α) • 1 + (α • s + star (α • s)) ∈ qmod R

If 1 - s⋆ s ∈ M, then (1 + |α|²)·1 + (α s + (α s)⋆) ∈ M for every α : ℂ: it is (1 + α s)⋆ (1 + α s) + |α|² (1 - s⋆ s).

theorem MIPRE.NCPoly.archimedean_of_gen {G : Type u_1} {R : Set (NCPoly G)} (hgen : ∀ (g : G), 1 - gen g * gen g ∈ qmod R) (y : NCPoly G) : ∃ (N : ℝ), N • 1 + y ∈ qmod R

The Archimedean property. If 1 - g² ∈ M for every letter g, then every polynomial is bounded by a multiple of the unit: N • 1 + y ∈ M for some real N.

The taxicab ℓ¹ norm

theorem MIPRE.NCPoly.taxicab_add_le (a b : ℂ) : |(a + b).re| + |(a + b).im| ≤ |a.re| + |a.im| + (|b.re| + |b.im|)

The taxicab norm of a complex number is subadditive.

theorem MIPRE.NCPoly.taxicab_mul_le (a b : ℂ) : |(a * b).re| + |(a * b).im| ≤ (|a.re| + |a.im|) * (|b.re| + |b.im|)

The taxicab norm of a complex number is submultiplicative.

def MIPRE.NCPoly.l1 {G : Type u_1} (z : NCPoly G) : ℝ

The taxicab ℓ¹ norm of a polynomial: the sum over words of |Re c_w| + |Im c_w|. It is the norm in which the exact certificates of the Tsirelson route are rounded (planning/tsirelson-campaign.md, §3.5).

Equations

• z.l1 = ∑ w ∈ z.coeff.support, (|(z.coeff w).re| + |(z.coeff w).im|)

theorem MIPRE.NCPoly.l1_eq_sum_of_subset {G : Type u_1} (z : NCPoly G) {s : Finset (FreeMonoid G)} (hs : z.coeff.support ⊆ s) : z.l1 = ∑ w ∈ s, (|(z.coeff w).re| + |(z.coeff w).im|)

The ℓ¹ norm, as a sum over any finite set of words containing the support.

theorem MIPRE.NCPoly.l1_nonneg {G : Type u_1} (z : NCPoly G) : 0 ≤ z.l1

The ℓ¹ norm is nonnegative.

@[simp]

theorem MIPRE.NCPoly.l1_zero {G : Type u_1} : l1 0 = 0

The ℓ¹ norm of 0.

@[simp]

theorem MIPRE.NCPoly.l1_single {G : Type u_1} (w : FreeMonoid G) (c : ℂ) : (single w c).l1 = |c.re| + |c.im|

The ℓ¹ norm of a monomial is the taxicab norm of its coefficient.

theorem MIPRE.NCPoly.l1_add_le {G : Type u_1} (x y : NCPoly G) : (x + y).l1 ≤ x.l1 + y.l1

The ℓ¹ norm is subadditive.

@[simp]

theorem MIPRE.NCPoly.l1_neg {G : Type u_1} (z : NCPoly G) : (-z).l1 = z.l1

The ℓ¹ norm is invariant under negation.

theorem MIPRE.NCPoly.l1_smul_le {G : Type u_1} (c : ℂ) (z : NCPoly G) : (c • z).l1 ≤ (|c.re| + |c.im|) * z.l1

The ℓ¹ norm of a complex multiple is at most the taxicab norm of the scalar times the ℓ¹ norm.

theorem MIPRE.NCPoly.l1_sum_le {G : Type u_1} {ι : Type u_2} (s : Finset ι) (f : ι → NCPoly G) : (∑ i ∈ s, f i).l1 ≤ ∑ i ∈ s, (f i).l1

The ℓ¹ norm of a finite sum is at most the sum of the norms.

@[simp]

theorem MIPRE.NCPoly.l1_star {G : Type u_1} (z : NCPoly G) : (star z).l1 = z.l1

The ℓ¹ norm is invariant under the star: it conjugates the coefficients and permutes the words.

theorem MIPRE.NCPoly.l1_mul_le {G : Type u_1} (x y : NCPoly G) : (x * y).l1 ≤ x.l1 * y.l1

The ℓ¹ norm is submultiplicative.

Separation by a nonnegative functional

theorem MIPRE.exists_nonneg_functional_of_archimedean {E : Type u_1} [AddCommGroup E] [Module ℝ E] (M : PointedCone ℝ E) (u : E) (harch : ∀ (y : E), ∃ (N : ℝ), N • u + y ∈ M) (hneg : -u ∉ M) : ∃ (L : E →ₗ[ℝ] ℝ), L u = 1 ∧ ∀ x ∈ M, 0 ≤ L x

Riesz extension for an order unit. If u is an order unit of a pointed cone M in a real vector space (∀ y, ∃ N, N • u + y ∈ M) and -u ∉ M, then some linear functional is nonnegative on M and takes the value 1 at u.

theorem MIPRE.exists_separating_functional_of_archimedean {E : Type u_1} [AddCommGroup E] [Module ℝ E] (M : PointedCone ℝ E) (u : E) (harch : ∀ (y : E), ∃ (N : ℝ), N • u + y ∈ M) (hu : u ∈ M) (h : E) (hh : h ∉ M) : ∃ (L : E →ₗ[ℝ] ℝ), L u = 1 ∧ (∀ x ∈ M, 0 ≤ L x) ∧ L h ≤ 0

Archimedean separation. If u ∈ M is an order unit of a pointed cone M in a real vector space and h ∉ M, then some linear functional is nonnegative on M, takes the value 1 at u, and is ≤ 0 at h.