Two continuous linear maps agreeing on a dense range

theorem CommutingRepetition.Density.clm_ext_of_denseRange {H : Type u_1} {K : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] {ι : Type u_3} {f : ι → H} (hf : DenseRange f) {S T : H →L[ℂ] K} (h : ∀ (i : ι), S (f i) = T (f i)) : S = T

theorem CommutingRepetition.Density.clm_ext_inner_of_denseRange {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {ι : Type u_2} {f : ι → H} (hf : DenseRange f) {S T : H →L[ℂ] H} (h : ∀ (i j : ι), inner ℂ (f i) (S (f j)) = inner ℂ (f i) (T (f j))) : S = T

An operator determined by its matrix coefficients on a dense range.

The contraction between the GNS spaces of dominated functionals

noncomputable def CommutingRepetition.Density.gnsCompressPre {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (ω ρ : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ ρ (star a * a)) : ρ.PreGNS →L[ℂ] ω.PreGNS

The identity of 𝒞 as a contraction PreGNS ρ → PreGNS ω, for ω ≤ ρ.

Equations

• CommutingRepetition.Density.gnsCompressPre ω ρ hle = (↑ω.toPreGNS ∘ₗ ↑ρ.ofPreGNS).mkContinuous 1 ⋯

noncomputable def CommutingRepetition.Density.gnsCompress {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (ω ρ : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ ρ (star a * a)) : ρ.GNS →L[ℂ] ω.GNS

The contraction GNS ρ → GNS ω induced by ω ≤ ρ.

Equations

• CommutingRepetition.Density.gnsCompress ω ρ hle = (CommutingRepetition.Density.gnsCompressPre ω ρ hle).completion

theorem CommutingRepetition.Density.gnsCompress_ιGNS {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (ω ρ : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ ρ (star a * a)) (a : 𝒞) : (gnsCompress ω ρ hle) ((ιGNS ρ) a) = (ιGNS ω) a

theorem CommutingRepetition.Density.gnsCompress_gns {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (ω ρ : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ ρ (star a * a)) (m : 𝒞) : gnsCompress ω ρ hle ∘SL ρ.gnsStarAlgHom m = ω.gnsStarAlgHom m ∘SL gnsCompress ω ρ hle

The conjugated functional τ_σ = τ(σ* · σ) and the isometry GNS(τ_σ) → GNS(τ)

noncomputable def CommutingRepetition.Density.conjState {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) : 𝒞 →ₚ[ℂ] ℂ

τ_σ(a) := τ(σ* a σ).

Equations

• CommutingRepetition.Density.conjState τ σ = PositiveLinearMap.mk₀ (τ.toLinearMap ∘ₗ LinearMap.mulLeft ℂ (star σ) ∘ₗ LinearMap.mulRight ℂ σ) ⋯

theorem CommutingRepetition.Density.conjState_apply {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ a : 𝒞) : (conjState τ σ) a = τ (star σ * (a * σ))

noncomputable def CommutingRepetition.Density.embedPre {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) : (conjState τ σ).PreGNS →L[ℂ] τ.PreGNS

x ↦ x σ as an isometry PreGNS τ_σ → PreGNS τ.

Equations

• CommutingRepetition.Density.embedPre τ σ = (↑τ.toPreGNS ∘ₗ LinearMap.mulRight ℂ σ ∘ₗ ↑(CommutingRepetition.Density.conjState τ σ).ofPreGNS).mkContinuous 1 ⋯

theorem CommutingRepetition.Density.embedPre_apply {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (x : (conjState τ σ).PreGNS) : (embedPre τ σ) x = τ.toPreGNS ((conjState τ σ).ofPreGNS x * σ)

noncomputable def CommutingRepetition.Density.embed {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) : (conjState τ σ).GNS →L[ℂ] τ.GNS

The isometry GNS(τ_σ) → GNS(τ), [a] ↦ ι(aσ).

Equations

• CommutingRepetition.Density.embed τ σ = (CommutingRepetition.Density.embedPre τ σ).completion

theorem CommutingRepetition.Density.embed_ιGNS {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ a : 𝒞) : (embed τ σ) ((ιGNS (conjState τ σ)) a) = (ιGNS τ) (a * σ)

theorem CommutingRepetition.Density.inner_embed {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (u v : (conjState τ σ).GNS) : inner ℂ ((embed τ σ) u) ((embed τ σ) v) = inner ℂ u v

theorem CommutingRepetition.Density.adjoint_embed_comp_embed {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) : ContinuousLinearMap.adjoint (embed τ σ) ∘SL embed τ σ = ContinuousLinearMap.id ℂ (conjState τ σ).GNS

theorem CommutingRepetition.Density.gns_comp_embed {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ m : 𝒞) : τ.gnsStarAlgHom m ∘SL embed τ σ = embed τ σ ∘SL (conjState τ σ).gnsStarAlgHom m

theorem CommutingRepetition.Density.adjoint_gns {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (ρ : 𝒞 →ₚ[ℂ] ℂ) (m : 𝒞) : ContinuousLinearMap.adjoint (ρ.gnsStarAlgHom m) = ρ.gnsStarAlgHom (star m)

theorem CommutingRepetition.Density.adjoint_embed_comp_gns {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ m : 𝒞) : ContinuousLinearMap.adjoint (embed τ σ) ∘SL τ.gnsStarAlgHom m = (conjState τ σ).gnsStarAlgHom m ∘SL ContinuousLinearMap.adjoint (embed τ σ)

noncomputable def CommutingRepetition.Density.cyclicProj {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) : τ.GNS →L[ℂ] τ.GNS

The projection onto the closure of L(𝒞) ι σ.

Equations

• CommutingRepetition.Density.cyclicProj τ σ = CommutingRepetition.Density.embed τ σ ∘SL ContinuousLinearMap.adjoint (CommutingRepetition.Density.embed τ σ)

theorem CommutingRepetition.Density.cyclicProj_embed {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (u : (conjState τ σ).GNS) : (cyclicProj τ σ) ((embed τ σ) u) = (embed τ σ) u

theorem CommutingRepetition.Density.cyclicProj_comp_gns {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ m : 𝒞) : cyclicProj τ σ ∘SL τ.gnsStarAlgHom m = τ.gnsStarAlgHom m ∘SL cyclicProj τ σ

theorem CommutingRepetition.Density.cyclicProj_mul_self {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) : cyclicProj τ σ * cyclicProj τ σ = cyclicProj τ σ

theorem CommutingRepetition.Density.adjoint_cyclicProj {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) : ContinuousLinearMap.adjoint (cyclicProj τ σ) = cyclicProj τ σ

theorem CommutingRepetition.Density.one_sub_cyclicProj_isPositive {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) : (1 - cyclicProj τ σ).IsPositive

theorem CommutingRepetition.Density.one_sub_cyclicProj_ι {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ a : 𝒞) : (1 - cyclicProj τ σ) ((ιGNS τ) (a * σ)) = 0

The Radon–Nikodym operator of a dominated functional

noncomputable def CommutingRepetition.Density.rnV {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (ω : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ (conjState τ σ) (star a * a)) : τ.GNS →L[ℂ] ω.GNS

V := gnsCompress ∘ embed*.

Equations

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

noncomputable def CommutingRepetition.Density.rnOp {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (ω : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ (conjState τ σ) (star a * a)) : τ.GNS →L[ℂ] τ.GNS

The Radon–Nikodym operator G = V* V.

Equations

• CommutingRepetition.Density.rnOp τ σ ω hle = ContinuousLinearMap.adjoint (CommutingRepetition.Density.rnV τ σ ω hle) ∘SL CommutingRepetition.Density.rnV τ σ ω hle

theorem CommutingRepetition.Density.rnOp_isPositive {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (ω : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ (conjState τ σ) (star a * a)) : (rnOp τ σ ω hle).IsPositive

theorem CommutingRepetition.Density.rnV_embed {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (ω : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ (conjState τ σ) (star a * a)) (u : (conjState τ σ).GNS) : (rnV τ σ ω hle) ((embed τ σ) u) = (gnsCompress ω (conjState τ σ) hle) u

theorem CommutingRepetition.Density.inner_rnOp {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (ω : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ (conjState τ σ) (star a * a)) (a c : 𝒞) : inner ℂ ((ιGNS τ) (a * σ)) ((rnOp τ σ ω hle) ((ιGNS τ) (c * σ))) = ω (star a * c)

The matrix coefficients: ⟪ι(aσ), G ι(cσ)⟫ = ω(a* c).

theorem CommutingRepetition.Density.rnOp_comp_gns {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (ω : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ (conjState τ σ) (star a * a)) (m : 𝒞) : rnOp τ σ ω hle ∘SL τ.gnsStarAlgHom m = τ.gnsStarAlgHom m ∘SL rnOp τ σ ω hle

G commutes with the left regular representation.

theorem CommutingRepetition.Density.rnOp_commute {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (ω : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ (conjState τ σ) (star a * a)) (m : 𝒞) : Commute (rnOp τ σ ω hle) (τ.gnsStarAlgHom m)

theorem CommutingRepetition.Density.cyclicProj_commute {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ m : 𝒞) : Commute (cyclicProj τ σ) (τ.gnsStarAlgHom m)

Assembly

theorem CommutingRepetition.Density.rnOp_eq {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) (ω : 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (a : 𝒞), ω (star a * a) ≤ (conjState τ σ) (star a * a)) (a : 𝒞) : rnOp τ σ ω hle = embed τ σ ∘SL (ContinuousLinearMap.adjoint (gnsCompress ω (conjState τ σ) hle) ∘SL gnsCompress ω (conjState τ σ) hle) ∘SL ContinuousLinearMap.adjoint (embed τ σ)

G = embed ∘ (C* C) ∘ embed*.

theorem CommutingRepetition.Density.sum_rnOp {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) {ι : Type u_1} [Fintype ι] (ω : ι → 𝒞 →ₚ[ℂ] ℂ) (hle : ∀ (i : ι) (a : 𝒞), (ω i) (star a * a) ≤ (conjState τ σ) (star a * a)) (hsum : ∀ (a : 𝒞), ∑ i : ι, (ω i) a = (conjState τ σ) a) : ∑ i : ι, rnOp τ σ (ω i) ⋯ = cyclicProj τ σ

If dominated functionals sum to τ_σ, their Radon–Nikodym operators sum to the cyclic projection.

theorem CommutingRepetition.Density.exists_traciallyEmbeddable {𝒞 : Type} [CStarAlgebra 𝒞] [PartialOrder 𝒞] [StarOrderedRing 𝒞] (τ : 𝒞 →ₚ[ℂ] ℂ) (σ : 𝒞) {Xc Ac : Type} [Fintype Xc] [Fintype Ac] [Nonempty Ac] (hτ1 : τ 1 = 1) (hτ : ∀ (a b : 𝒞), τ (a * b) = τ (b * a)) (hσ : 0 ≤ σ) (hσ1 : τ (σ * σ) = 1) (E : Xc → Ac → 𝒞) (hE0 : ∀ (x : Xc) (a : Ac), 0 ≤ E x a) (hE1 : ∀ (x : Xc), ∑ a : Ac, E x a = 1) (ω : Xc → Ac → 𝒞 →ₚ[ℂ] ℂ) (hω : ∀ (y : Xc) (a : 𝒞), ∑ b : Ac, (ω y b) a = (conjState τ σ) a) : ∃ (q : TraciallyEmbeddableCorrelation Xc Ac), ∀ (x y : Xc) (a b : Ac), q.toCorrelation x y a b = ((ω y b) (E x a)).re

The tracially embeddable package of a tracial state τ, a positive σ with τ(σ²) = 1, Alice POVMs in 𝒞, and Bob given by positive functionals ω_b^y summing to τ(σ · σ): the correlation is re ω_b^y(E_a^x).