The game algebra of Tsirelson's problem

The algebraic layer of the Tsirelson route (planning/tsirelson-campaign.md, §3.1–§3.2): the free ⋆-algebra of a two-player scenario with question sets X, Y and answer sets A, B, its cone of positive elements, and the correspondence between commuting-operator strategies and states on it.

The algebra. The letters are Gen X Y A B = (X × A) ⊕ (Y × B), one self-adjoint letter eG x a per effect of the first player and fG y b per effect of the second, and the algebra is NCPoly (Gen X Y A B). The relations rels are the two POVM normalisations Σ_a e_xa - 1, Σ_b f_yb - 1 and the cross commutators e_xa f_yb - f_yb e_xa; the cone M = cone X Y A B is their quadratic module NCPoly.qmod. Every letter satisfies 1 - g ∈ M (1 - e_xa = Σ_{a' ≠ a} e_xa' - (Σ_a' e_xa' - 1)), hence 1 - g² ∈ M (one_sub_gen_mul_gen_mem), so M is Archimedean (cone_archimedean), and a polynomial outside M is separated from it by a real functional (exists_state_functional_of_not_mem).

Strategies. A commuting-operator strategy S evaluates the letters at its effects (stratEval S), which kills the relations, so every element of M has nonnegative expectation in the strategy's state (strategy_nonneg). The correlation is the expectation of e_xa f_yb (correlation_eq), and the value in a game G is the expectation of the game polynomial W_G = gamePoly G = Σ μ(x, y) [D x y a b] e_xa f_yb (value_eq). Hence a cone certificate r·1 - W_G ∈ M bounds every strategy's value, and the commuting-operator value, by r (value_le_of_mem, commutingOperatorValue_le_of_mem). The latter is stated for 0 ≤ r, which lets it use Real.iSup_le without a nonemptiness hypothesis; it cannot be dropped: if A is empty and X is not, then -1 = Σ_a e_xa - 1 is a relation, the cone is the whole algebra, and there is no strategy, so the value is 0. Every effect, and so every word, evaluates to a contraction (norm_eval_single_one_le).

Cone states. A cone state (IsConeState) is a ℂ-linear functional L with L 1 = 1 and 0 ≤ Re L m for every m ∈ M. This single notion covers the three sources of states:

• the state stateOf S : z ↦ ⟪ψ, π_S(z) ψ⟫ of a strategy is a cone state (isConeState_stateOf), bounded by 1 on words (norm_stateOf_single_one_le);
• the complexification z ↦ L₀ z - i L₀ (i z) of a real functional that is 1 at the unit and nonnegative on M is a cone state (complexify, isConeState_complexify), so a polynomial outside M is separated from it by a cone state (exists_isConeState_of_not_mem);
• a cone state is hermitian (IsConeState.map_star, since z - z⋆ and i (z + z⋆) are anti-hermitian), vanishes on the relation ideal (IsConeState.map_eq_zero_of_mem_relSpan, since ±j, ±i j ∈ M), and is positive on every s⋆ g s; so it is a GNS.State whose letters form GNS.GenData, and the GNS construction turns it into a commuting-operator strategy stateStrategy hL with correlation Re L (e_xa f_yb) and value Re L (W_G) (stateStrategy_correlation, stateStrategy_value).

Together: C_qc is exactly the set of the Re L (e_xa f_yb) over cone states L (mem_Cqc_iff). The GNS part needs X Y A B : Type, since the Hilbert space of a CommutingOperatorStrategy lives in Type.

Finally, the deterministic strategy on ℂ (CommutingOperatorStrategy.deterministic) makes the type of strategies nonempty when both answer sets are (CommutingOperatorStrategy.instNonempty), which uniform bounds over strategies need for ciSup_le.

Main declarations

• Gen, eG, fG, rels, cone, one_sub_eG_mem, one_sub_fG_mem, one_sub_gen_mul_gen_mem, cone_archimedean, exists_state_functional_of_not_mem;
• stratEval, stratEval_rels, strategy_nonneg, correlation_eq, gamePoly, value_eq, value_le_of_mem, commutingOperatorValue_le_of_mem;
• stateOf, IsConeState, isConeState_stateOf, complexify, isConeState_complexify, exists_isConeState_of_not_mem;
• IsConeState.toState, IsConeState.genData, stateStrategy, stateStrategy_correlation, stateStrategy_value, re_gamePoly_le_commutingOperatorValue, mem_Cqc_iff;
• CommutingOperatorStrategy.deterministic, CommutingOperatorStrategy.norm_E_le_one, CommutingOperatorStrategy.norm_F_le_one.

The deterministic strategy, and contractions

noncomputable def MIPRE.CommutingOperatorStrategy.deterministic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (a₀ : A) (b₀ : B) : CommutingOperatorStrategy X Y A B

The deterministic strategy on ℂ that always answers (a₀, b₀): every effect is 1 or 0.

Equations

• One or more equations did not get rendered due to their size.

instance MIPRE.CommutingOperatorStrategy.instNonempty {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] : Nonempty (CommutingOperatorStrategy X Y A B)

There is a commuting-operator strategy as soon as both answer sets are nonempty.

theorem MIPRE.CommutingOperatorStrategy.norm_E_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (a : A) : ‖S.E x a‖ ≤ 1

Every effect of the first player is a contraction: 0 ≤ E x a ≤ 1.

theorem MIPRE.CommutingOperatorStrategy.norm_F_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (b : B) : ‖S.F y b‖ ≤ 1

Every effect of the second player is a contraction: 0 ≤ F y b ≤ 1.

Letters, relations, and the cone

@[reducible, inline]

abbrev MIPRE.Tsirelson.Gen (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) : Type (max (max u_3 u_1) u_4 u_2)

The letters of the game algebra: one per effect E x a and one per effect F y b.

Equations

• MIPRE.Tsirelson.Gen X Y A B = (X × A ⊕ Y × B)

noncomputable def MIPRE.Tsirelson.eG {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (x : X) (a : A) : NCPoly (Gen X Y A B)

The letter e_xa, standing for the first player's effect E x a.

Equations

• MIPRE.Tsirelson.eG x a = MIPRE.NCPoly.gen (Sum.inl (x, a))

noncomputable def MIPRE.Tsirelson.fG {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (y : Y) (b : B) : NCPoly (Gen X Y A B)

The letter f_yb, standing for the second player's effect F y b.

Equations

• MIPRE.Tsirelson.fG y b = MIPRE.NCPoly.gen (Sum.inr (y, b))

@[simp]

theorem MIPRE.Tsirelson.star_eG {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (x : X) (a : A) : star (eG x a) = eG x a

The letters e_xa are self-adjoint.

@[simp]

theorem MIPRE.Tsirelson.star_fG {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (y : Y) (b : B) : star (fG y b) = fG y b

The letters f_yb are self-adjoint.

def MIPRE.Tsirelson.rels (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype A] [Fintype B] : Set (NCPoly (Gen X Y A B))

The relations of the game algebra: both POVM normalisations Σ_a e_xa - 1, Σ_b f_yb - 1, and the cross commutators e_xa f_yb - f_yb e_xa.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev MIPRE.Tsirelson.cone (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype A] [Fintype B] : PointedCone ℝ (NCPoly (Gen X Y A B))

The cone M of the game algebra: the quadratic module of rels.

Equations

• MIPRE.Tsirelson.cone X Y A B = MIPRE.NCPoly.qmod (MIPRE.Tsirelson.rels X Y A B)

theorem MIPRE.Tsirelson.sum_eG_sub_one_mem_relSpan {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (x : X) : ∑ a : A, eG x a - 1 ∈ NCPoly.relSpan (rels X Y A B)

The first player's normalisation lies in the relation ideal.

theorem MIPRE.Tsirelson.sum_fG_sub_one_mem_relSpan {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (y : Y) : ∑ b : B, fG y b - 1 ∈ NCPoly.relSpan (rels X Y A B)

The second player's normalisation lies in the relation ideal.

theorem MIPRE.Tsirelson.commutator_mem_relSpan {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (x : X) (y : Y) (a : A) (b : B) : eG x a * fG y b - fG y b * eG x a ∈ NCPoly.relSpan (rels X Y A B)

The cross commutators lie in the relation ideal.

theorem MIPRE.Tsirelson.one_sub_eG_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (x : X) (a : A) : 1 - eG x a ∈ cone X Y A B

1 - e_xa ∈ M: it is Σ_{a' ≠ a} e_xa' - (Σ_a' e_xa' - 1).

theorem MIPRE.Tsirelson.one_sub_fG_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (y : Y) (b : B) : 1 - fG y b ∈ cone X Y A B

1 - f_yb ∈ M: it is Σ_{b' ≠ b} f_yb' - (Σ_b' f_yb' - 1).

theorem MIPRE.Tsirelson.one_sub_gen_mul_gen_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (g : Gen X Y A B) : 1 - NCPoly.gen g * NCPoly.gen g ∈ cone X Y A B

Every letter g of the game algebra satisfies 1 - g² ∈ M.

theorem MIPRE.Tsirelson.cone_archimedean {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (y : NCPoly (Gen X Y A B)) : ∃ (N : ℝ), N • 1 + y ∈ cone X Y A B

The Archimedean property of the game cone: every polynomial is bounded by a multiple of the unit.

theorem MIPRE.Tsirelson.exists_state_functional_of_not_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {h : NCPoly (Gen X Y A B)} (hh : h ∉ cone X Y A B) : ∃ (L : NCPoly (Gen X Y A B) →ₗ[ℝ] ℝ), L 1 = 1 ∧ (∀ m ∈ cone X Y A B, 0 ≤ L m) ∧ L h ≤ 0

Separation from the game cone. A polynomial outside M is separated from it by a real linear functional that is nonnegative on M, takes the value 1 at the unit, and is ≤ 0 at the polynomial.

Evaluation in a strategy

def MIPRE.Tsirelson.stratEval {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : Gen X Y A B → S.H →L[ℂ] S.H

The letters evaluated in a commuting-operator strategy: e_xa ↦ E x a, f_yb ↦ F y b.

Equations

• MIPRE.Tsirelson.stratEval S = Sum.elim (fun (p : X × A) => S.E p.1 p.2) fun (p : Y × B) => S.F p.1 p.2

@[simp]

theorem MIPRE.Tsirelson.eval_eG {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (a : A) : (NCPoly.eval (stratEval S)) (eG x a) = S.E x a

The letter e_xa evaluates to the effect E x a.

@[simp]

theorem MIPRE.Tsirelson.eval_fG {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (b : B) : (NCPoly.eval (stratEval S)) (fG y b) = S.F y b

The letter f_yb evaluates to the effect F y b.

theorem MIPRE.Tsirelson.stratEval_isPositive {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (g : Gen X Y A B) : (stratEval S g).IsPositive

The letters evaluate to positive operators.

theorem MIPRE.Tsirelson.norm_stratEval_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (g : Gen X Y A B) : ‖stratEval S g‖ ≤ 1

The letters evaluate to contractions.

theorem MIPRE.Tsirelson.norm_eval_single_one_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (w : FreeMonoid (Gen X Y A B)) : ‖(NCPoly.eval (stratEval S)) (NCPoly.single w 1)‖ ≤ 1

Every word evaluates to a contraction.

theorem MIPRE.Tsirelson.stratEval_rels {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (ρ : NCPoly (Gen X Y A B)) : ρ ∈ rels X Y A B → (NCPoly.eval (stratEval S)) ρ = 0

The strategy satisfies the relations.

theorem MIPRE.Tsirelson.strategy_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) {m : NCPoly (Gen X Y A B)} (hm : m ∈ cone X Y A B) : 0 ≤ (inner ℂ S.ψ (((NCPoly.eval (stratEval S)) m) S.ψ)).re

Positivity of the cone in every strategy: every element of M has nonnegative expectation in the strategy's state.

theorem MIPRE.Tsirelson.correlation_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : S.correlation x y a b = (inner ℂ S.ψ (((NCPoly.eval (stratEval S)) (eG x a * fG y b)) S.ψ)).re

The correlation of a strategy is the expectation of e_xa f_yb.

noncomputable def MIPRE.Tsirelson.gamePoly {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : NCPoly (Gen X Y A B)

The game polynomial W_G = Σ μ(x, y) [D x y a b] e_xa f_yb, with real coefficients.

Equations

• MIPRE.Tsirelson.gamePoly G = ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, ↑(G.μ x y * if G.D x y a b = true then 1 else 0) • (MIPRE.Tsirelson.eG x a * MIPRE.Tsirelson.fG y b)

theorem MIPRE.Tsirelson.value_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) : CommutingOperatorStrategy.value G S = (inner ℂ S.ψ (((NCPoly.eval (stratEval S)) (gamePoly G)) S.ψ)).re

The value of a strategy is the expectation of the game polynomial.

theorem MIPRE.Tsirelson.value_le_of_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) {r : ℝ} (h : r • 1 - gamePoly G ∈ cone X Y A B) : CommutingOperatorStrategy.value G S ≤ r

Soundness of a cone certificate: r·1 - W_G ∈ M bounds every strategy's value by r.

theorem MIPRE.Tsirelson.commutingOperatorValue_le_of_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {r : ℝ} (hr : 0 ≤ r) (h : r • 1 - gamePoly G ∈ cone X Y A B) : commutingOperatorValue G ≤ r

The commuting-operator value under a cone certificate: r·1 - W_G ∈ M with 0 ≤ r bounds the commuting-operator value by r. The sign hypothesis replaces nonemptiness of the type of strategies (Real.iSup_le); it cannot be dropped, since if A is empty and X is not, every polynomial lies in the cone.

The state of a strategy

noncomputable def MIPRE.Tsirelson.stateOf {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ

The state of a strategy on the game algebra: z ↦ ⟪ψ, π_S(z) ψ⟫, with π_S the evaluation of the letters in the strategy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Tsirelson.stateOf_apply {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (z : NCPoly (Gen X Y A B)) : (stateOf S) z = inner ℂ S.ψ (((NCPoly.eval (stratEval S)) z) S.ψ)

The state of a strategy, applied.

theorem MIPRE.Tsirelson.norm_stateOf_single_one_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (w : FreeMonoid (Gen X Y A B)) : ‖(stateOf S) (NCPoly.single w 1)‖ ≤ 1

The state of a strategy is bounded by 1 on every word.

theorem MIPRE.Tsirelson.re_stateOf_eG_mul_fG {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : ((stateOf S) (eG x a * fG y b)).re = S.correlation x y a b

The state of a strategy recovers its correlation.

theorem MIPRE.Tsirelson.re_stateOf_gamePoly {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) : ((stateOf S) (gamePoly G)).re = CommutingOperatorStrategy.value G S

The state of a strategy recovers its value.

Cone states

structure MIPRE.Tsirelson.IsConeState {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ) : Prop

A cone state on the game algebra: a ℂ-linear functional that is 1 at the unit and has nonnegative real part on the cone M.

• map_one : L 1 = 1

  A cone state is normalized.

• re_nonneg (m : NCPoly (Gen X Y A B)) : m ∈ cone X Y A B → 0 ≤ (L m).re

  A cone state has nonnegative real part on the cone.

theorem MIPRE.Tsirelson.IsConeState.re_eq_zero_of_neg_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) {m : NCPoly (Gen X Y A B)} (hm : m ∈ cone X Y A B) (hm' : -m ∈ cone X Y A B) : (L m).re = 0

A cone state has vanishing real part on m when both m and -m lie in the cone.

theorem MIPRE.Tsirelson.IsConeState.re_eq_zero_of_star_eq_neg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) {z : NCPoly (Gen X Y A B)} (hz : star z = -z) : (L z).re = 0

A cone state has vanishing real part on anti-hermitian elements.

theorem MIPRE.Tsirelson.IsConeState.map_star {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) (z : NCPoly (Gen X Y A B)) : L (star z) = (starRingEnd ℂ) (L z)

A cone state is hermitian: z - z⋆ and i (z + z⋆) are anti-hermitian.

theorem MIPRE.Tsirelson.IsConeState.map_eq_zero_of_mem_relSpan {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) {z : NCPoly (Gen X Y A B)} (hz : z ∈ NCPoly.relSpan (rels X Y A B)) : L z = 0

A cone state vanishes on the relation ideal: ±j and ±i j lie in it.

theorem MIPRE.Tsirelson.IsConeState.map_mul_mul_eq_zero {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) {j : NCPoly (Gen X Y A B)} (hj : j ∈ NCPoly.relSpan (rels X Y A B)) (u v : NCPoly (Gen X Y A B)) : L (u * j * v) = 0

A cone state vanishes on u j v for j in the relation ideal.

theorem MIPRE.Tsirelson.IsConeState.re_star_mul_self_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) (a : NCPoly (Gen X Y A B)) : 0 ≤ (L (star a * a)).re

A cone state is positive on hermitian squares.

theorem MIPRE.Tsirelson.isConeState_stateOf {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] [Fintype X] [Fintype Y] (S : CommutingOperatorStrategy X Y A B) : IsConeState (stateOf S)

The state of a strategy is a cone state.

Complexification of a real functional

def MIPRE.Tsirelson.complexify {P : Type u_1} [AddCommGroup P] [Module ℂ P] (L₀ : P →ₗ[ℝ] ℝ) : P →ₗ[ℂ] ℂ

The complexification z ↦ L₀ z - i L₀ (i z) of a real linear functional on a complex vector space: the unique ℂ-linear functional with real part L₀.

Equations

• MIPRE.Tsirelson.complexify L₀ = { toFun := fun (z : P) => ↑(L₀ z) - Complex.I * ↑(L₀ (Complex.I • z)), map_add' := ⋯, map_smul' := ⋯ }

theorem MIPRE.Tsirelson.complexify_apply {P : Type u_1} [AddCommGroup P] [Module ℂ P] (L₀ : P →ₗ[ℝ] ℝ) (z : P) : (complexify L₀) z = ↑(L₀ z) - Complex.I * ↑(L₀ (Complex.I • z))

The complexification, applied.

@[simp]

theorem MIPRE.Tsirelson.re_complexify {P : Type u_1} [AddCommGroup P] [Module ℂ P] (L₀ : P →ₗ[ℝ] ℝ) (z : P) : ((complexify L₀) z).re = L₀ z

The real part of the complexification is the original functional.

theorem MIPRE.Tsirelson.isConeState_complexify {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {L₀ : NCPoly (Gen X Y A B) →ₗ[ℝ] ℝ} (h1 : L₀ 1 = 1) (hM : ∀ m ∈ cone X Y A B, 0 ≤ L₀ m) : IsConeState (complexify L₀)

The complexification of a real functional that is 1 at the unit and nonnegative on the cone is a cone state.

theorem MIPRE.Tsirelson.exists_isConeState_of_not_mem {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {h : NCPoly (Gen X Y A B)} (hh : h ∉ cone X Y A B) : ∃ (L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ), IsConeState L ∧ (L h).re ≤ 0

Separation by a cone state. A polynomial outside the cone is separated from it by a cone state with nonpositive real part at the polynomial.

The GNS strategy of a cone state

def MIPRE.Tsirelson.IsConeState.toState {X Y A B : Type} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) : GNS.State (NCPoly (Gen X Y A B))

A cone state as a GNS.State of the game algebra.

Equations

• hL.toState = { L := L, map_one := ⋯, map_star := ⋯, nonneg := ⋯ }

@[simp]

theorem MIPRE.Tsirelson.IsConeState.toState_L {X Y A B : Type} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) : hL.toState.L = L

The functional of the GNS.State of a cone state is the cone state.

noncomputable def MIPRE.Tsirelson.IsConeState.genData {X Y A B : Type} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} (hL : IsConeState L) : GNS.GenData (NCPoly (Gen X Y A B)) X Y A B hL.toState

The letters satisfy, under a cone state, the relations of two commuting families of POVMs.

Equations

• hL.genData = { e := MIPRE.Tsirelson.eG, f := MIPRE.Tsirelson.fG, e_sa := ⋯, f_sa := ⋯, e_pos := ⋯, f_pos := ⋯, e_sum := ⋯, f_sum := ⋯, comm := ⋯ }

noncomputable def MIPRE.Tsirelson.stateStrategy {X Y A B : Type} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} [Fintype X] [Fintype Y] (hL : IsConeState L) : CommutingOperatorStrategy X Y A B

The GNS strategy of a cone state.

Equations

• MIPRE.Tsirelson.stateStrategy hL = hL.genData.strategy

theorem MIPRE.Tsirelson.stateStrategy_correlation {X Y A B : Type} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} [Fintype X] [Fintype Y] (hL : IsConeState L) (x : X) (y : Y) (a : A) (b : B) : (stateStrategy hL).correlation x y a b = (L (eG x a * fG y b)).re

The correlation of the GNS strategy of a cone state is Re L (e_xa f_yb).

theorem MIPRE.Tsirelson.stateStrategy_value {X Y A B : Type} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} [Fintype X] [Fintype Y] (hL : IsConeState L) (G : Game X Y A B) : CommutingOperatorStrategy.value G (stateStrategy hL) = (L (gamePoly G)).re

The value of the GNS strategy of a cone state is Re L (W_G).

theorem MIPRE.Tsirelson.re_gamePoly_le_commutingOperatorValue {X Y A B : Type} [Fintype A] [Fintype B] {L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ} [Fintype X] [Fintype Y] (hL : IsConeState L) (G : Game X Y A B) : (L (gamePoly G)).re ≤ commutingOperatorValue G

A cone state is bounded on the game polynomial by the commuting-operator value.

theorem MIPRE.Tsirelson.mem_Cqc_iff {X Y A B : Type} [Fintype A] [Fintype B] [Fintype X] [Fintype Y] {p : X → Y → A → B → ℝ} : p ∈ Cqc X Y A B ↔ ∃ (L : NCPoly (Gen X Y A B) →ₗ[ℂ] ℂ), IsConeState L ∧ p = fun (x : X) (y : Y) (a : A) (b : B) => (L (eG x a * fG y b)).re

C_qc through cone states: the commuting-operator correlations are exactly the Re L (e_xa f_yb) for cone states L.