The von Neumann algebra generated by a set

noncomputable def CommutingRepetition.VN.wstar {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) : VonNeumannAlgebra H

The von Neumann algebra generated by S: the bicommutant of S ∪ star S.

Equations

• CommutingRepetition.VN.wstar S = { toStarSubalgebra := StarSubalgebra.centralizer ℂ ↑(StarSubalgebra.centralizer ℂ S), centralizer_centralizer' := ⋯ }

theorem CommutingRepetition.VN.mem_wstar_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {T : H →L[ℂ] H} : T ∈ wstar S ↔ ∀ y ∈ StarSubalgebra.centralizer ℂ S, y * T = T * y

theorem CommutingRepetition.VN.subset_wstar {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {s : H →L[ℂ] H} (hs : s ∈ S) : s ∈ wstar S

theorem CommutingRepetition.VN.mem_of_commute_commutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {T : H →L[ℂ] H} (h : ∀ y ∈ N.commutant, y * T = T * y) : T ∈ N

An element commuting with the commutant of N lies in N (the definition of a von Neumann algebra).

theorem CommutingRepetition.VN.commutant_mul_of_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {N : VonNeumannAlgebra H} {T y : H →L[ℂ] H} (hT : T ∈ N) (hy : y ∈ N.commutant) : y * T = T * y

theorem CommutingRepetition.VN.wstar_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {N : VonNeumannAlgebra H} (h : S ⊆ ↑N) {T : H →L[ℂ] H} (hT : T ∈ wstar S) : T ∈ N

wstar S is the smallest von Neumann algebra containing S.

Closure under strong limits and functional calculi

theorem CommutingRepetition.VN.mem_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {ι : Type u_2} {l : Filter ι} [l.NeBot] {T : ι → H →L[ℂ] H} {L : H →L[ℂ] H} (hT : ∀ (i : ι), T i ∈ N) (h : ∀ (ξ : H), Filter.Tendsto (fun (i : ι) => (T i) ξ) l (nhds (L ξ))) : L ∈ N

A von Neumann algebra is closed under pointwise (strong) limits of bounded or unbounded nets: the commutation relations pass to the limit.

theorem CommutingRepetition.VN.cfc_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {T : H →L[ℂ] H} (hT : T ∈ N) (f : ℂ → ℂ) : cfc f T ∈ N

theorem CommutingRepetition.VN.cfc_real_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {T : H →L[ℂ] H} (hT : T ∈ N) (f : ℝ → ℝ) : cfc f T ∈ N

theorem CommutingRepetition.VN.bfc_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {E : H →L[ℂ] H} (hE : IsSelfAdjoint E) (hEN : E ∈ N) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : BorelCalc.bfc E hE g ∈ N

theorem CommutingRepetition.VN.mem_of_tendsto_seq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (N : VonNeumannAlgebra H) {T : ℕ → H →L[ℂ] H} {L : H →L[ℂ] H} (hT : ∀ (n : ℕ), T n ∈ N) (h : ∀ (ξ : H), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) : L ∈ N

Pointwise limits of sequences: the form used for monotone and Cesàro limits.