noncomputable def CommutingRepetition.VN.sfXi {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) : Hinf H

The vector Ξ = (gₖ) ∈ ℓ²(ℕ, H).

Equations

• CommutingRepetition.VN.sfXi g hg = CommutingRepetition.VN.mkVec g hg

theorem CommutingRepetition.VN.sfXi_separating {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) : IsSeparating (↑(amplAlg N)) (sfXi g hg)

noncomputable def CommutingRepetition.VN.sfSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) : Submodule ℂ (Hinf H)

The standard-form Hilbert space K = [(N ⊗ 1) Ξ].

Equations

• CommutingRepetition.VN.sfSpace N g hg = CommutingRepetition.VN.cyclicSpace (↑(CommutingRepetition.VN.amplAlg N)) (CommutingRepetition.VN.sfXi g hg)

instance CommutingRepetition.VN.instCompleteSpaceSubtypeHinfMemSubmoduleComplexSfSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) : CompleteSpace ↥(sfSpace N g hg)

theorem CommutingRepetition.VN.sfSpace_invariant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) (x : Hinf H →L[ℂ] Hinf H) : x ∈ amplAlg N → ∀ v ∈ sfSpace N g hg, x v ∈ sfSpace N g hg

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

noncomputable def CommutingRepetition.VN.sfVec {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (g : ℕ → H) (hg : Summable fun (k : ℕ) => ‖g k‖ ^ 2) : ↥(sfSpace N g hg)

The vector Ξ as an element of K.

Equations

• CommutingRepetition.VN.sfVec N g hg = ⟨CommutingRepetition.VN.sfXi g hg, ⋯⟩

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

noncomputable def CommutingRepetition.VN.sfAlg {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) : VonNeumannAlgebra ↥(sfSpace N g hg)

The standard-form von Neumann algebra M = P (N ⊗ 1) ι on K.

Equations

• CommutingRepetition.VN.sfAlg N g hg hfaith = CommutingRepetition.VN.cutdown (CommutingRepetition.VN.sfSpace N g hg) (CommutingRepetition.VN.amplAlg N) ⋯ (CommutingRepetition.VN.sfXi g hg) ⋯ ⋯

theorem CommutingRepetition.VN.sfVec_isCyclic {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) : IsCyclic (↑(sfAlg N g hg hfaith)) (sfVec N g hg)

theorem CommutingRepetition.VN.sfVec_isSeparating {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) : IsSeparating (↑(sfAlg N g hg hfaith)) (sfVec N g hg)

noncomputable def CommutingRepetition.VN.sfMap {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) : ↥(sfSpace N g hg) →L[ℂ] ↥(sfSpace N g hg)

The map θ : B(H) → B(K), T ↦ P (T ⊗ 1) ι.

Equations

• CommutingRepetition.VN.sfMap N g hg T = CommutingRepetition.VN.compressTo (CommutingRepetition.VN.sfSpace N g hg) (CommutingRepetition.VN.ampl T)

theorem CommutingRepetition.VN.sfMap_mem {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) {x : H →L[ℂ] H} (hx : x ∈ N) : sfMap N g hg x ∈ sfAlg N g hg hfaith

theorem CommutingRepetition.VN.sfMap_surjective {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) {S : ↥(sfSpace N g hg) →L[ℂ] ↥(sfSpace N g hg)} (hS : S ∈ sfAlg N g hg hfaith) : ∃ x ∈ N, sfMap N g hg x = S

theorem CommutingRepetition.VN.sfMap_injective {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) {x y : H →L[ℂ] H} (hx : x ∈ N) (hy : y ∈ N) (h : sfMap N g hg x = sfMap N g hg y) : x = y

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

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

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

theorem CommutingRepetition.VN.sfMap_star {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) : sfMap N g hg (star x) = star (sfMap N g hg x)

theorem CommutingRepetition.VN.sfMap_mul {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) {y : H →L[ℂ] H} (hy : y ∈ N) : sfMap N g hg (x * y) = sfMap N g hg x * sfMap N g hg y

theorem CommutingRepetition.VN.norm_sfMap_le {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) : ‖sfMap N g hg x‖ ≤ ‖x‖

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

θ is normal.

theorem CommutingRepetition.VN.inner_sfVec_sfMap {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) : inner ℂ (sfVec N g hg) ((sfMap N g hg T) (sfVec N g hg)) = ∑' (k : ℕ), inner ℂ (g k) (T (g k))

⟪Ξ, θ(T) Ξ⟫ = ∑ₖ ⟪gₖ, T gₖ⟫: the vector state of Ξ is φ.

theorem CommutingRepetition.VN.coe_sfMap_apply {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) (hT : T ∈ N) (v : ↥(sfSpace N g hg)) : ↑((sfMap N g hg T) v) = (ampl T) ↑v

theorem CommutingRepetition.VN.tendstoStrongBdd_of_sfMap {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) {ι : Type u_2} {l : Filter ι} {T : ι → H →L[ℂ] H} {L : H →L[ℂ] H} (hT : ∀ (i : ι), T i ∈ N) (hL : L ∈ N) {C : ℝ} (hC : ∀ (i : ι), ‖T i‖ ≤ C) (h : Filter.Tendsto (fun (i : ι) => (sfMap N g hg (T i)) (sfVec N g hg)) l (nhds ((sfMap N g hg L) (sfVec N g hg)))) : TendstoStrongBdd l T L

The inverse of θ is normal: bounded convergence of θ(T i) Ξ alone forces bounded strong convergence of T i on H.