Documentation

MIPRE.Background.Repetition.CommutingRepetition.Tracial.Density.CrossedTracial

Positivity and finite sums for π, amp and Φ_n #

source
theorem CommutingRepetition.Density.π_finset_sum {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {ι : Type u_2} (s : Finset ι) (f : ι → K →L[ℂ] K) :
VN.Crossed.π M Ω (∑ i ∈ s, f i) = ∑ i ∈ s, VN.Crossed.π M Ω (f i)
source
theorem CommutingRepetition.Density.amp_finset_sum {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {ι : Type u_2} (s : Finset ι) (f : ι → K →L[ℂ] K) :
VN.Crossed.amp (∑ i ∈ s, f i) = ∑ i ∈ s, VN.Crossed.amp (f i)
source
theorem CommutingRepetition.Density.π_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {y : K →L[ℂ] K} (hy : 0 ≤ y) :
0 ≤ VN.Crossed.π M Ω y

π preserves positivity: y = c*c gives π y = (π c)*(π c).

source
theorem CommutingRepetition.Density.amp_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {y : K →L[ℂ] K} (hy : 0 ≤ y) :
0 ≤ VN.Crossed.amp y

amp preserves positivity.

source
theorem CommutingRepetition.Density.Phi_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) :
VN.Haagerup.Phi M Ω n 0 = 0
source
theorem CommutingRepetition.Density.Phi_finset_sum {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) {ι : Type u_2} (s : Finset ι) (f : ι → VN.Crossed.L2Q K →L[ℂ] VN.Crossed.L2Q K) :
VN.Haagerup.Phi M Ω n (∑ i ∈ s, f i) = ∑ i ∈ s, VN.Haagerup.Phi M Ω n (f i)

e^{r a_n} lies in ℛ_n #

source
theorem CommutingRepetition.Density.expA_an_mem_Rn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : VN.IsSeparating (↑M) Ω) (hc : VN.IsCyclic (↑M) Ω) (n : ℕ) (r : ℝ) :
VN.Modular.expA (VN.Haagerup.an n) r ∈ VN.Haagerup.Rn M Ω n
source
theorem CommutingRepetition.Density.dn_mem_Rn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : VN.IsSeparating (↑M) Ω) (hc : VN.IsCyclic (↑M) Ω) (n : ℕ) :
VN.Haagerup.dn n ∈ VN.Haagerup.Rn M Ω n

Alice and Bob inside the crossed product #

source
noncomputable def CommutingRepetition.Density.StdStrategy.Ai {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (x : X) (a : A) :
VN.Crossed.L2Q q.K →L[ℂ] VN.Crossed.L2Q q.K

Alice's effect, transported into the crossed product by π.

Equations
Instances For
    source
    noncomputable def CommutingRepetition.Density.StdStrategy.Bi {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (y : Y) (b : B) :
    VN.Crossed.L2Q q.K →L[ℂ] VN.Crossed.L2Q q.K

    Bob's effect, transported into the commutant of the crossed product by amp.

    Equations
    Instances For
      source
      theorem CommutingRepetition.Density.StdStrategy.Ai_def {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (x : X) (a : A) :
      q.Ai x a = VN.Crossed.π q.M q.Ω (q.Aop x a)
      source
      theorem CommutingRepetition.Density.StdStrategy.Bi_def {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (y : Y) (b : B) :
      q.Bi y b = VN.Crossed.amp (q.Bop y b)
      source
      theorem CommutingRepetition.Density.StdStrategy.Ai_mem {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (x : X) (a : A) :
      q.Ai x a ∈ VN.Crossed.crossed q.M q.Ω
      source
      theorem CommutingRepetition.Density.StdStrategy.Ai_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (x : X) (a : A) :
      0 ≤ q.Ai x a
      source
      theorem CommutingRepetition.Density.StdStrategy.Ai_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (x : X) :
      ∑ a : A, q.Ai x a = 1
      source
      theorem CommutingRepetition.Density.StdStrategy.Bi_mem_commutant {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (y : Y) (b : B) :
      q.Bi y b ∈ (VN.Crossed.crossed q.M q.Ω).commutant
      source
      theorem CommutingRepetition.Density.StdStrategy.Bi_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (y : Y) (b : B) :
      0 ≤ q.Bi y b
      source
      theorem CommutingRepetition.Density.StdStrategy.Bi_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (y : Y) :
      ∑ b : B, q.Bi y b = 1
      source
      theorem CommutingRepetition.Density.StdStrategy.norm_Bi_le {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) [DecidableEq B] (y : Y) (b : B) :
      ‖q.Bi y b‖ ≤ 1
      source
      theorem CommutingRepetition.Density.StdStrategy.Bi_commute {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) {z : VN.Crossed.L2Q q.K →L[ℂ] VN.Crossed.L2Q q.K} (hz : z ∈ VN.Crossed.crossed q.M q.Ω) (y : Y) (b : B) :
      Commute z (q.Bi y b)
      source
      theorem CommutingRepetition.Density.StdStrategy.inner_Ωh_Ai_Bi {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) :
      inner ℂ (VN.Crossed.Ωh q.Ω) ((q.Ai x a) ((q.Bi y b) (VN.Crossed.Ωh q.Ω))) = inner ℂ q.Ω ((q.Aop x a) ((q.Bop y b) q.Ω))

      The crossed product reproduces the correlation of q.

      The tracial data at level n #

      source
      theorem CommutingRepetition.Density.StdStrategy.xin_eq {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (n : ℕ) :
      VN.Haagerup.xin q.Ω n = (VN.Modular.expA (VN.Haagerup.an n) (-(1 / 2))) (VN.Crossed.Ωh q.Ω)
      source
      theorem CommutingRepetition.Density.StdStrategy.norm_Ωh_eq_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) :
      ‖VN.Crossed.Ωh q.Ω‖ = 1
      source
      theorem CommutingRepetition.Density.StdStrategy.norm_xin_pos {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (n : ℕ) :
      0 < ‖VN.Haagerup.xin q.Ω n‖
      source
      theorem CommutingRepetition.Density.StdStrategy.inner_xin_dn {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) (n : ℕ) :
      inner ℂ (VN.Haagerup.xin q.Ω n) ((VN.Haagerup.dn n) (VN.Haagerup.xin q.Ω n)) = 1

      ⟪ξ_n, d_n ξ_n⟫ = 1: the density d_n transports ψ_{ξ_n} back to the unit state.

      The tracial approximation #

      source
      theorem CommutingRepetition.Density.StdStrategy.exists_tracial_approx {Xc Ac : Type} [Fintype Xc] [Fintype Ac] [Nonempty Ac] (q : StdStrategy Xc Xc Ac Ac) {η : ℝ} (hη : 0 < η) :
      ∃ (t : TraciallyEmbeddableCorrelation Xc Ac), ∀ (x y : Xc) (a b : Ac), |t.toCorrelation x y a b - q.corr x y a b| ≤ η

      Stage E7.3: the correlation of a standard-form commuting strategy is entrywise η-close to a tracially embeddable correlation.