def CommutingRepetition.l1Dist {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (p q : Correlation X Y A B) : ℝ

ℓ¹ distance between two correlation tables on common finite alphabets.

Equations

• CommutingRepetition.l1Dist p q = ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, |p x y a b - q x y a b|

structure CommutingRepetition.TraciallyEmbeddableCorrelation (Xc Ac : Type) [Fintype Xc] [Fintype Ac] : Type 1

A tracially embeddable correlation on common alphabets, in the exact shape of Lin's Definition 3.1: standard form of a tracial algebra, density σ ∈ M₊ with τ(σ²) = 1, Alice POVMs in M acting on the left, Bob POVMs given by positive operators in the COMMUTANT of the left action.

• M : StdTracialAlgebra
• σ : self.M.A
• σ_pos : IsPosElem self.σ
• σ_normalized : self.M.τ (star self.σ * self.σ) = 1
• E : Xc → Ac → self.M.A
• E_pos (x : Xc) (a : Ac) : IsPosElem (self.E x a)
• E_sum (x : Xc) : ∑ a : Ac, self.E x a = 1
• G : Xc → Ac → self.M.H →L[ℂ] self.M.H
• G_pos (y : Xc) (b : Ac) : (self.G y b).IsPositive
• G_sum (y : Xc) : ∑ b : Ac, self.G y b = 1
• G_commutant (y : Xc) (b : Ac) (m : self.M.A) : Commute (self.G y b) (self.M.L m)

noncomputable def CommutingRepetition.TraciallyEmbeddableCorrelation.toCorrelation {Xc Ac : Type} [Fintype Xc] [Fintype Ac] (q : TraciallyEmbeddableCorrelation Xc Ac) : Correlation Xc Xc Ac Ac

The correlation table realized by a tracially embeddable strategy in commutant form: p(a, b | x, y) = ⟪ι σ, L(E_x^a) G_y^b (ι σ)⟫.

Equations

• q.toCorrelation x y a b = (inner ℂ (q.M.ι q.σ) ((q.M.L (q.E x a)) ((q.G y b) (q.M.ι q.σ)))).re

theorem CommutingRepetition.TraciallyEmbeddableCorrelation.toCorrelation_isCommuting {Xc Ac : Type} [Fintype Xc] [Fintype Ac] (q : TraciallyEmbeddableCorrelation Xc Ac) : IsCommutingCorrelation q.toCorrelation

Every tracially embeddable correlation is a commuting-operator correlation — the easy inclusion C_qc^Tr ⊆ C_qc, realized on the standard-form Hilbert space with state ι σ, Alice through the left representation and Bob's commutant effects as given.

def CommutingRepetition.TracialDensityHypothesis : Prop

The tracial density hypothesis (Lin, arXiv:2304.01940, Thm 3.2): for all finite common alphabets, every commuting-operator correlation is an ℓ¹-limit of tracially embeddable correlations. It is never an axiom, and since stage E7 it is proved — Density.tracialDensity in Tracial/Density/Main.lean — so the root theorems no longer take it as a hypothesis. MainStatement.tracialDensity is the same theorem in the vocabulary of the standalone Statement.lean.

Equations

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