Physicslib4.Operators.DensityTheorem

The von Neumann density theorem

For a unital *-algebra homomorphism ρ : 𝔄 →⋆ₐ[ℂ] (E →L[ℂ] E) on a complex Hilbert space E, every element of the bicommutant ρ(𝔄)'' is a strong limit of elements of ρ(𝔄). This file proves the ingredients: the one-vector case (for T ∈ ρ(𝔄)'' and ξ ∈ E, T ξ lies in the closure of ρ(𝔄) ξ), the diagonal amplification ρ^ι on ℓ²(ι; E), and the fact that diag(T) ∈ (ρ^ι(𝔄))'' for a finite index type ι. The commutant is Set.centralizer, as in Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean.

Blueprint reference: lmm:cyclic-subspace-reduces, lmm:bicommutant-single-vector, def:finite-amplification, lmm:commutant-of-amplification-entries, lmm:amplification-block-expansion, lmm:diagonal-in-amplified-bicommutant.

Supporting lemmas

• blockEntry_apply — unfolds blockEntry to its defining composite; feeds blockEntry_mem_centralizer (lmm:commutant-of-amplification-entries).

theorem Physicslib4.starProjection_cyclic_mem_centralizer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄] (ρ : 𝔄 →⋆ₐ[ℂ] E →L[ℂ] E) (ξ : E) : (Submodule.span ℂ (Set.range fun (a : 𝔄) => (ρ a) ξ)).topologicalClosure.starProjection ∈ (Set.range ⇑ρ).centralizer

The cyclic subspace of a vector reduces the representation. The orthogonal projection onto the closed subspace closure (ρ(𝔄) ξ) commutes with every ρ a.

Blueprint reference: lmm:cyclic-subspace-reduces.

theorem Physicslib4.apply_mem_closure_of_mem_bicommutant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄] (ρ : 𝔄 →⋆ₐ[ℂ] E →L[ℂ] E) {T : E →L[ℂ] E} (hT : T ∈ (Set.range ⇑ρ).centralizer.centralizer) (ξ : E) : T ξ ∈ closure (Set.range fun (a : 𝔄) => (ρ a) ξ)

The bicommutant moves a vector within its cyclic subspace. For T ∈ ρ(𝔄)'' and ξ ∈ E, T ξ lies in the closure of ρ(𝔄) ξ; unitality of ρ puts ξ itself in that closure.

Blueprint reference: lmm:bicommutant-single-vector.

The amplification of a representation

For an index type ι, the amplification ρ^ι acts on ℓ²(ι; E) by the diagonal operator diag(ρ a, ρ a, …). Every copy is bounded by ‖ρ a‖, so no norm on 𝔄 is needed (unlike Physicslib4.GNS.directSum, which bounds different representations through a C*-norm). Finite index types are used for the density theorem.

noncomputable def Physicslib4.ampDiag {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ι : Type u_3) (T : E →L[ℂ] E) : ↥(lp (fun (x : ι) => E) 2) →L[ℂ] ↥(lp (fun (x : ι) => E) 2)

The diagonal operator diag(T, T, …) on ℓ²(ι; E).

Blueprint reference: def:finite-amplification.

Equations

• Physicslib4.ampDiag ι T = Physicslib4.lpDiag (fun (x : ι) => T) ⋯ ⋯

@[simp]

theorem Physicslib4.ampDiag_apply_coe {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ι : Type u_3) (T : E →L[ℂ] E) (x : ↥(lp (fun (x : ι) => E) 2)) (i : ι) : ↑((ampDiag ι T) x) i = T (↑x i)

noncomputable def Physicslib4.diagAmplification {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄] (ι : Type u_3) (ρ : 𝔄 →⋆ₐ[ℂ] E →L[ℂ] E) : 𝔄 →⋆ₐ[ℂ] ↥(lp (fun (x : ι) => E) 2) →L[ℂ] ↥(lp (fun (x : ι) => E) 2)

The amplification ρ^ι of a unital *-representation ρ on ℓ²(ι; E): ρ^ι(a) = diag(ρ a, ρ a, …).

Blueprint reference: def:finite-amplification, lmm:finite-amplification-star-hom.

Equations

• Physicslib4.diagAmplification ι ρ = { toFun := fun (a : 𝔄) => Physicslib4.ampDiag ι (ρ a), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem Physicslib4.diagAmplification_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄] (ι : Type u_3) (ρ : 𝔄 →⋆ₐ[ℂ] E →L[ℂ] E) (a : 𝔄) : (diagAmplification ι ρ) a = ampDiag ι (ρ a)

noncomputable def Physicslib4.toLp2 {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_3} [Finite ι] (ξ : ι → E) : ↥(lp (fun (x : ι) => E) 2)

A finite family of vectors as an element of ℓ²(ι; E).

Equations

• Physicslib4.toLp2 ξ = ⟨ξ, ⋯⟩

@[simp]

theorem Physicslib4.toLp2_apply {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_3} [Finite ι] (ξ : ι → E) (i : ι) : ↑(toLp2 ξ) i = ξ i

Block entries and the diagonal of the bicommutant

noncomputable def Physicslib4.blockEntry {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ι : Type u_3} [DecidableEq ι] (S : ↥(lp (fun (x : ι) => E) 2) →L[ℂ] ↥(lp (fun (x : ι) => E) 2)) (j k : ι) : E →L[ℂ] E

The block entry S_{jk} = (coordinate j) ∘ S ∘ (inclusion k) of an operator on ℓ²(ι; E).

Blueprint reference: lmm:commutant-of-amplification-entries.

Equations

• Physicslib4.blockEntry S j k = lp.evalCLM ℂ (fun (x : ι) => E) 2 j ∘SL S ∘SL lp.singleContinuousLinearMap ℂ (fun (x : ι) => E) 2 k

theorem Physicslib4.blockEntry_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ι : Type u_3} [DecidableEq ι] (S : ↥(lp (fun (x : ι) => E) 2) →L[ℂ] ↥(lp (fun (x : ι) => E) 2)) (j k : ι) (v : E) : (blockEntry S j k) v = ↑(S (lp.single 2 k v)) j

theorem Physicslib4.blockEntry_mem_centralizer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄] {ι : Type u_3} [DecidableEq ι] (ρ : 𝔄 →⋆ₐ[ℂ] E →L[ℂ] E) {S : ↥(lp (fun (x : ι) => E) 2) →L[ℂ] ↥(lp (fun (x : ι) => E) 2)} (hS : S ∈ (Set.range ⇑(diagAmplification ι ρ)).centralizer) (j k : ι) : blockEntry S j k ∈ (Set.range ⇑ρ).centralizer

The block entries of an operator commuting with the amplification commute with ρ.

Blueprint reference: lmm:commutant-of-amplification-entries.

theorem Physicslib4.apply_eq_sum_blockEntry {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ι : Type u_3} [DecidableEq ι] [Fintype ι] (S : ↥(lp (fun (x : ι) => E) 2) →L[ℂ] ↥(lp (fun (x : ι) => E) 2)) (x : ↥(lp (fun (x : ι) => E) 2)) (j : ι) : ↑(S x) j = ∑ k : ι, (blockEntry S j k) (↑x k)

Block expansion. On a finite index type, (S x)_j = ∑ₖ S_{jk} (x k).

Blueprint reference: lmm:amplification-block-expansion.

theorem Physicslib4.ampDiag_mem_bicommutant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄] {ι : Type u_3} [Finite ι] (ρ : 𝔄 →⋆ₐ[ℂ] E →L[ℂ] E) {T : E →L[ℂ] E} (hT : T ∈ (Set.range ⇑ρ).centralizer.centralizer) : ampDiag ι T ∈ (Set.range ⇑(diagAmplification ι ρ)).centralizer.centralizer

The diagonal of a bicommutant element lies in the amplified bicommutant. If T ∈ ρ(𝔄)'', then diag(T, …, T) ∈ (ρ^ι(𝔄))'' for a finite index type ι.

Blueprint reference: lmm:diagonal-in-amplified-bicommutant.

Finitely many vectors at once

theorem Physicslib4.exists_forall_norm_sub_lt_of_mem_bicommutant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄] (ρ : 𝔄 →⋆ₐ[ℂ] E →L[ℂ] E) {T : E →L[ℂ] E} (hT : T ∈ (Set.range ⇑ρ).centralizer.centralizer) {s : Set E} (hs : s.Finite) {ε : ℝ} (hε : 0 < ε) : ∃ (a : 𝔄), ∀ x ∈ s, ‖T x - (ρ a) x‖ < ε

Finitely many vectors at once. For T ∈ ρ(𝔄)'', a finite set s of vectors and ε > 0, some a has ‖T x - ρ a x‖ < ε for every x ∈ s. (Apply the one-vector case to the amplification over s, to diag(T) and to the family s ↪ E.)

Blueprint reference: lmm:bicommutant-finite-vectors.