The von Neumann density theorem

Let S be a unital star subalgebra of the bounded operators on a Hilbert space H over ℝ or ℂ. Every operator x in the double commutant S'' is a strong-operator limit of elements of S: for finitely many vectors v i and every ε > 0 there is s ∈ S with ‖x (v i) - s (v i)‖ < ε for all i, StarSubalgebra.exists_forall_norm_sub_apply_lt_of_mem_centralizer_centralizer.

For a von Neumann algebra generated by a set s of operators on a complex Hilbert space, every element of VonNeumannAlgebra.adjoin s is approximated in this sense by elements of the star algebra generated by s, VonNeumannAlgebra.exists_forall_norm_sub_apply_lt_of_mem_adjoin.

For a single vector v this is StarSubalgebra.apply_mem_closure_of_mem_centralizer_centralizer. The closure K of the orbit S v is invariant under S, and so is its orthogonal complement because S is closed under adjoints. Hence the orthogonal projection onto K lies in the commutant S' and commutes with x; since v ∈ K, this gives x v ∈ K.

Finitely many vectors are handled by amplification: S acts diagonally on the Hilbert sum PiLp 2 (fun _ : ι => H) through PiLp.diagStarAlgHom. Every operator on this sum commuting with the diagonal copy of S has matrix entries (ContinuousLinearMap.piLpEntry) in S', so the diagonal copy of x lies in the double commutant of the diagonal copy of S, and the single-vector case applies to the sum.

Simultaneous approximation on finitely many vectors is what lets an identity between vector functionals y ↦ ⟪u, y v⟫, proved for y in the range π(A) of a representation, pass to the von Neumann algebra π(A)'' that it generates.

References

Kadison–Ringrose, Fundamentals of the Theory of Operator Algebras I, Theorem 5.3.1, for the double commutant theorem and its amplification proof.

theorem StarSubalgebra.apply_mem_closure_of_mem_centralizer_centralizer {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) {x : H →L[𝕜] H} (hx : x ∈ (↑S).centralizer.centralizer) (v : H) : x v ∈ closure ((fun (s : H →L[𝕜] H) => s v) '' ↑S)

The von Neumann density theorem for one vector. An operator in the double commutant of a unital star subalgebra S maps each vector v into the closure of the orbit S v.

theorem StarSubalgebra.exists_forall_norm_sub_apply_lt_of_mem_centralizer_centralizer {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) {x : H →L[𝕜] H} (hx : x ∈ (↑S).centralizer.centralizer) {ι : Type u_3} [Finite ι] (v : ι → H) {ε : ℝ} (hε : 0 < ε) : ∃ s ∈ S, ∀ (i : ι), ‖x (v i) - s (v i)‖ < ε

The von Neumann density theorem. An operator x in the double commutant of a unital star subalgebra S of the bounded operators on a Hilbert space is a strong-operator limit of elements of S: for every finite family of vectors v i and every ε > 0 there is s ∈ S with ‖x (v i) - s (v i)‖ < ε for all i.

theorem VonNeumannAlgebra.exists_forall_norm_sub_apply_lt_of_mem_adjoin {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : Set (H →L[ℂ] H)} {x : H →L[ℂ] H} (hx : x ∈ adjoin s) {ι : Type u_2} [Finite ι] (v : ι → H) {ε : ℝ} (hε : 0 < ε) : ∃ t ∈ StarAlgebra.adjoin ℂ s, ∀ (i : ι), ‖x (v i) - t (v i)‖ < ε

The von Neumann density theorem for a generated von Neumann algebra. An operator x in the von Neumann algebra generated by a set s of bounded operators is a strong-operator limit of elements of the star algebra generated by s: for every finite family of vectors v i and every ε > 0 there is t ∈ StarAlgebra.adjoin ℂ s with ‖x (v i) - t (v i)‖ < ε for all i.