More on J

theorem CommutingRepetition.StdTracialAlgebra.J_traceVector (M : StdTracialAlgebra) : M.J M.traceVector = M.traceVector

theorem CommutingRepetition.StdTracialAlgebra.norm_J (M : StdTracialAlgebra) (v : M.H) : ‖M.J v‖ = ‖v‖

theorem CommutingRepetition.StdTracialAlgebra.J_L_J (M : StdTracialAlgebra) (a : M.A) (v : M.H) : M.J ((M.L a) (M.J v)) = (M.Rop (star a)) v

J L(a) J = R(a*).

noncomputable def CommutingRepetition.StdTracialAlgebra.conjJ (M : StdTracialAlgebra) (G : M.H →L[ℂ] M.H) : M.H →L[ℂ] M.H

Conjugation by J, G ↦ J G J, as a (linear) bounded operator.

Equations

• M.conjJ G = { toFun := fun (v : M.H) => M.J (G (M.J v)), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖G‖ ⋯

theorem CommutingRepetition.StdTracialAlgebra.conjJ_apply (M : StdTracialAlgebra) (G : M.H →L[ℂ] M.H) (v : M.H) : (M.conjJ G) v = M.J (G (M.J v))

theorem CommutingRepetition.StdTracialAlgebra.conjJ_one (M : StdTracialAlgebra) : M.conjJ 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.conjJ_sum (M : StdTracialAlgebra) {ι : Type u_1} (s : Finset ι) (G : ι → M.H →L[ℂ] M.H) : M.conjJ (∑ i ∈ s, G i) = ∑ i ∈ s, M.conjJ (G i)

theorem CommutingRepetition.StdTracialAlgebra.conjJ_mem_vnAlg (M : StdTracialAlgebra) {G : M.H →L[ℂ] M.H} (hG : ∀ (m : M.A), Commute G (M.L m)) : M.conjJ G ∈ M.vnAlg

J G J commutes with the right action when G commutes with the left action.

theorem CommutingRepetition.StdTracialAlgebra.conjJ_nonneg (M : StdTracialAlgebra) {G : M.H →L[ℂ] M.H} (hG : G.IsPositive) : 0 ≤ M.conjJ G

J G J is positive when G is.

theorem CommutingRepetition.StdTracialAlgebra.traceState_conjJ (M : StdTracialAlgebra) (σ E : M.A) {G : M.H →L[ℂ] M.H} (hsa : IsSelfAdjoint G) (hG : ∀ (m : M.A), Commute G (M.L m)) : M.traceState (M.L (star σ) * M.L E * M.L σ * M.conjJ G) = inner ℂ (M.ι σ) ((M.L E) (G (M.ι σ)))

The pullback identity: φ(L(σ)* L(E) L(σ) · JGJ) = ⟪ισ, L(E) G ισ⟫ for G in the commutant of the left action.

Positivity in vnAlg

theorem CommutingRepetition.StdTracialAlgebra.sqrt_mem_vnAlg (M : StdTracialAlgebra) {P : M.H →L[ℂ] M.H} (hP0 : 0 ≤ P) (hP : P ∈ M.vnAlg) : CFC.sqrt P ∈ M.vnAlg

theorem CommutingRepetition.StdTracialAlgebra.isPosElem_of_nonneg (M : StdTracialAlgebra) {T : M.H →L[ℂ] M.H} (hT0 : 0 ≤ T) (hT : T ∈ M.vnAlg) : IsPosElem ⟨T, hT⟩

A positive operator in vnAlg is algebraically positive there (a single square).

noncomputable def CommutingRepetition.StdTracialAlgebra.Lv (M : StdTracialAlgebra) (a : M.A) : ↥M.vnAlg

L a as an element of vnAlg M.

Equations

• M.Lv a = ⟨M.L a, ⋯⟩

theorem CommutingRepetition.StdTracialAlgebra.Lv_val (M : StdTracialAlgebra) (a : M.A) : ↑(M.Lv a) = M.L a

theorem CommutingRepetition.StdTracialAlgebra.Lv_mul (M : StdTracialAlgebra) (a b : M.A) : M.Lv (a * b) = M.Lv a * M.Lv b

theorem CommutingRepetition.StdTracialAlgebra.Lv_star (M : StdTracialAlgebra) (a : M.A) : M.Lv (star a) = star (M.Lv a)

theorem CommutingRepetition.StdTracialAlgebra.Lv_one (M : StdTracialAlgebra) : M.Lv 1 = 1

theorem CommutingRepetition.StdTracialAlgebra.coe_sum_vnAlg (M : StdTracialAlgebra) {ι : Type u_1} (s : Finset ι) (f : ι → ↥M.vnAlg) : ↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)

theorem CommutingRepetition.StdTracialAlgebra.Lv_sum (M : StdTracialAlgebra) {ι : Type u_1} (s : Finset ι) (f : ι → M.A) : M.Lv (∑ x ∈ s, f x) = ∑ x ∈ s, M.Lv (f x)

theorem CommutingRepetition.StdTracialAlgebra.isPosElem_Lv (M : StdTracialAlgebra) {a : M.A} (ha : IsPosElem a) : IsPosElem (M.Lv a)

The pulled-back tracial strategy

noncomputable def CommutingRepetition.TraciallyEmbeddableCorrelation.Fv {Xc Ac : Type} [Fintype Xc] [Fintype Ac] (q : TraciallyEmbeddableCorrelation Xc Ac) (y : Xc) (b : Ac) : ↥q.M.vnAlg

Bob's pulled-back effect J G J in vnAlg.

Equations

• q.Fv y b = ⟨q.M.conjJ (q.G y b), ⋯⟩

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

The tracial strategy realizing a commutant-form correlation (node 1.1.4): the model vnModel M, density L(σ), Alice's effects L(E), Bob's effects J G J.

Equations

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

theorem CommutingRepetition.TraciallyEmbeddableCorrelation.pullback_correlation {Xc Ac : Type} [Fintype Xc] [Fintype Ac] (q : TraciallyEmbeddableCorrelation Xc Ac) : q.pullback.correlation = q.toCorrelation

The pulled-back strategy reproduces the correlation.