The cyclic subspace

def CommutingRepetition.VN.orbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (S : Set (H →L[ℂ] H)) (ξ : H) : Submodule ℂ H

The linear span of {x ξ | x ∈ S}.

Equations

• CommutingRepetition.VN.orbit S ξ = Submodule.span ℂ ((fun (x : H →L[ℂ] H) => x ξ) '' S)

def CommutingRepetition.VN.cyclicSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (S : Set (H →L[ℂ] H)) (ξ : H) : Submodule ℂ H

The closed cyclic subspace [S ξ].

Equations

• CommutingRepetition.VN.cyclicSpace S ξ = (CommutingRepetition.VN.orbit S ξ).topologicalClosure

theorem CommutingRepetition.VN.isClosed_cyclicSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) (ξ : H) : IsClosed ↑(cyclicSpace S ξ)

instance CommutingRepetition.VN.completeSpace_cyclicSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) (ξ : H) : CompleteSpace ↥(cyclicSpace S ξ)

theorem CommutingRepetition.VN.apply_mem_orbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {ξ : H} {x : H →L[ℂ] H} (hx : x ∈ S) : x ξ ∈ orbit S ξ

theorem CommutingRepetition.VN.orbit_le_cyclicSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) (ξ : H) : orbit S ξ ≤ cyclicSpace S ξ

theorem CommutingRepetition.VN.apply_mem_cyclicSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {ξ : H} {x : H →L[ℂ] H} (hx : x ∈ S) : x ξ ∈ cyclicSpace S ξ

theorem CommutingRepetition.VN.mem_cyclicSpace_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : ξ ∈ cyclicSpace (↑N) ξ

theorem CommutingRepetition.VN.apply_mem_orbit_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) {x : H →L[ℂ] H} (hx : x ∈ N) {v : H} (hv : v ∈ orbit (↑N) ξ) : x v ∈ orbit (↑N) ξ

The orbit of a von Neumann algebra is invariant under the algebra.

theorem CommutingRepetition.VN.apply_mem_cyclicSpace_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) {x : H →L[ℂ] H} (hx : x ∈ N) {v : H} (hv : v ∈ cyclicSpace (↑N) ξ) : x v ∈ cyclicSpace (↑N) ξ

The cyclic subspace of a von Neumann algebra is invariant under the algebra.

noncomputable def CommutingRepetition.VN.cycProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : H →L[ℂ] H

The projection onto the cyclic subspace [N ξ].

Equations

• CommutingRepetition.VN.cycProj N ξ = (CommutingRepetition.VN.cyclicSpace (↑N) ξ).starProjection

theorem CommutingRepetition.VN.cycProj_isStarProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : IsStarProjection (cycProj N ξ)

theorem CommutingRepetition.VN.cycProj_range {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : (↑(cycProj N ξ)).range = cyclicSpace (↑N) ξ

theorem CommutingRepetition.VN.cycProj_mem_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : cycProj N ξ ∈ N.commutant

The projection onto [N ξ] lies in the commutant N′.

theorem CommutingRepetition.VN.cycProj_commutant_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : cycProj N.commutant ξ ∈ N

The projection onto [N′ ξ] lies in N.

theorem CommutingRepetition.VN.cycProj_apply_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : (cycProj N ξ) ξ = ξ

Cyclic and separating vectors

def CommutingRepetition.VN.IsCyclic {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (S : Set (H →L[ℂ] H)) (ξ : H) : Prop

ξ is cyclic for S: span (S ξ) is dense.

Equations

• CommutingRepetition.VN.IsCyclic S ξ = Dense ↑(CommutingRepetition.VN.orbit S ξ)

def CommutingRepetition.VN.IsSeparating {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (S : Set (H →L[ℂ] H)) (ξ : H) : Prop

ξ is separating for S: x ξ = 0 ⇒ x = 0 for x ∈ S.

Equations

• CommutingRepetition.VN.IsSeparating S ξ = ∀ x ∈ S, x ξ = 0 → x = 0

theorem CommutingRepetition.VN.IsCyclic.cyclicSpace_eq_top {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {ξ : H} (h : IsCyclic S ξ) : cyclicSpace S ξ = ⊤

theorem CommutingRepetition.VN.isCyclic_of_cyclicSpace_eq_top {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {ξ : H} (h : cyclicSpace S ξ = ⊤) : IsCyclic S ξ

theorem CommutingRepetition.VN.IsSeparating.isCyclic_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : VonNeumannAlgebra H} {ξ : H} (h : IsSeparating (↑N) ξ) : IsCyclic (↑N.commutant) ξ

A vector separating for N is cyclic for N′ ([N′ ξ]^⊥ is N-invariant, so its projection is in N and kills ξ).

theorem CommutingRepetition.VN.IsCyclic.isSeparating_of_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : VonNeumannAlgebra H} {ξ : H} (h : IsCyclic (↑N.commutant) ξ) : IsSeparating (↑N) ξ

A vector cyclic for N′ is separating for N.

theorem CommutingRepetition.VN.isSeparating_iff_isCyclic_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) (ξ : H) : IsSeparating (↑N) ξ ↔ IsCyclic (↑N.commutant) ξ

theorem CommutingRepetition.VN.IsSeparating.mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S T : Set (H →L[ℂ] H)} {ξ : H} (h : IsSeparating T ξ) (hST : S ⊆ T) : IsSeparating S ξ

theorem CommutingRepetition.VN.isSeparating_of_faithful {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {ξ : H} (h : ∀ x ∈ S, inner ℂ ξ ((star x * x) ξ) = 0 → x = 0) : IsSeparating S ξ

A vector state faithful on N gives a separating vector.

From convergence at a separating vector to strong convergence

theorem CommutingRepetition.VN.tendsto_of_dense {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_2} {l : Filter ι} {T : ι → H →L[ℂ] H} {L : H →L[ℂ] H} {C : ℝ} (hC : ∀ (i : ι), ‖T i‖ ≤ C) {s : Set H} (hs : Dense s) (h : ∀ v ∈ s, Filter.Tendsto (fun (i : ι) => (T i) v) l (nhds (L v))) (ξ : H) : Filter.Tendsto (fun (i : ι) => (T i) ξ) l (nhds (L ξ))

Bounded pointwise convergence on a dense set gives pointwise convergence everywhere.

theorem CommutingRepetition.VN.tendstoStrongBdd_of_tendsto_separating {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {ξ : H} (hξ : IsSeparating (↑N) ξ) {ι : 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 : ι) => (T i) ξ) l (nhds (L ξ))) : TendstoStrongBdd l T L

Convergence at a separating vector, with a uniform norm bound, upgrades to bounded strong convergence (the commutant orbit N′ ξ is dense and T i (y ξ) = y (T i ξ)).