sfMap beyond N

theorem CommutingRepetition.Density.exists_sqrt_op {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (h0 : 0 ≤ A) : ∃ (r : H →L[ℂ] H), IsSelfAdjoint r ∧ r * r = A

theorem CommutingRepetition.Density.norm_povm_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (E : ι → H →L[ℂ] H) (hpos : ∀ (i : ι), (E i).IsPositive) (hsum : ∑ i : ι, E i = 1) (i : ι) : ‖E i‖ ≤ 1

POVM elements are contractions.

theorem CommutingRepetition.Density.sfMap_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) : VN.sfMap N g hg 0 = 0

theorem CommutingRepetition.Density.sfMap_finset_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) {ι : Type u_2} (s : Finset ι) (f : ι → H →L[ℂ] H) : VN.sfMap N g hg (∑ i ∈ s, f i) = ∑ i ∈ s, VN.sfMap N g hg (f i)

theorem CommutingRepetition.Density.sfMap_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) {T : H →L[ℂ] H} (h0 : 0 ≤ T) : 0 ≤ VN.sfMap N g hg T

theorem CommutingRepetition.Density.sfMap_mul_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) {x : H →L[ℂ] H} (hx : x ∈ N) (T : H →L[ℂ] H) : VN.sfMap N g hg x * VN.sfMap N g hg T = VN.sfMap N g hg (x * T)

θ is multiplicative when the left factor is in N, for an arbitrary right factor.

theorem CommutingRepetition.Density.norm_sfVec_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) : ‖VN.sfVec N g hg‖ ^ 2 = ∑' (k : ℕ), ‖g k‖ ^ 2

theorem CommutingRepetition.Density.sfMap_mem_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) (hfaith : ∀ x ∈ N, ∑' (k : ℕ), inner ℂ (g k) ((star x * x) (g k)) = 0 → x = 0) {T : H →L[ℂ] H} (hT : T ∈ N.commutant) : VN.sfMap N g hg T ∈ (VN.sfAlg N g hg hfaith).commutant

Bob transports to the commutant: the compression of T ⊗ 1 for T ∈ N′ commutes with M = sfAlg.

Alice's algebra

def CommutingRepetition.Density.aliceSet {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : Set (S.H →L[ℂ] S.H)

Alice's effects, as a generating set.

Equations

• CommutingRepetition.Density.aliceSet S = {T : S.H →L[ℂ] S.H | ∃ (x : X) (a : A), T = S.E x a}

noncomputable def CommutingRepetition.Density.aliceAlg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : VonNeumannAlgebra S.H

Alice's von Neumann algebra.

Equations

• CommutingRepetition.Density.aliceAlg S = CommutingRepetition.VN.wstar (CommutingRepetition.Density.aliceSet S)

theorem CommutingRepetition.Density.E_mem_aliceAlg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (x : X) (a : A) : S.E x a ∈ aliceAlg S

theorem CommutingRepetition.Density.F_mem_aliceAlg_commutant {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) (y : Y) (b : B) : S.F y b ∈ (aliceAlg S).commutant

The packaged standard-form strategy

structure CommutingRepetition.Density.StdStrategy (X Y A B : Type) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type 1

A commuting strategy in standard form: a von Neumann algebra M with a cyclic separating unit vector Ω, Alice's POVM inside M and Bob's POVM inside M′.

• K : Type
• nacg : NormedAddCommGroup self.K
• ips : InnerProductSpace ℂ self.K
• cspace : CompleteSpace self.K
• M : VonNeumannAlgebra self.K
• Ω : self.K
• Ω_norm : ‖self.Ω‖ = 1
• sep : VN.IsSeparating (↑self.M) self.Ω
• cyc : VN.IsCyclic (↑self.M) self.Ω
• Aop : X → A → self.K →L[ℂ] self.K
• Aop_mem (x : X) (a : A) : self.Aop x a ∈ self.M
• Aop_nonneg (x : X) (a : A) : 0 ≤ self.Aop x a
• Aop_sum (x : X) : ∑ a : A, self.Aop x a = 1
• Bop : Y → B → self.K →L[ℂ] self.K
• Bop_mem (y : Y) (b : B) : self.Bop y b ∈ self.M.commutant
• Bop_nonneg (y : Y) (b : B) : 0 ≤ self.Bop y b
• Bop_sum (y : Y) : ∑ b : B, self.Bop y b = 1

noncomputable def CommutingRepetition.Density.StdStrategy.corr {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (q : StdStrategy X Y A B) : Correlation X Y A B

The correlation of a standard-form strategy.

Equations

• q.corr x y a b = (inner ℂ q.Ω ((q.Aop x a) ((q.Bop y b) q.Ω))).re

Construction

noncomputable def CommutingRepetition.Density.stdOf {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) [TopologicalSpace.SeparableSpace S.H] [Nonempty S.H] {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : StdStrategy X Y A B

The standard-form strategy attached to a separable commuting strategy and an ε ∈ (0,1).

Equations

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

theorem CommutingRepetition.Density.stdOf_corr {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) [TopologicalSpace.SeparableSpace S.H] [Nonempty S.H] {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (x : X) (y : Y) (a : A) (b : B) : (stdOf S hε0 hε1).corr x y a b = (gvecState S.ψ (TopologicalSpace.denseSeq S.H) ε (S.E x a * S.F y b)).re