SpatialMatrixDensity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Increasing finite spatial matrix images are weakly dense

theorem OAI.KadisonKastler.spatialRight_mem_generated_contraction line 21

theorem OAI.KadisonKastler.spatialRight_mem_generated line 44

Source documentation

The right spatial representation carries the generated von Neumann algebra into the von Neumann algebra generated by its images.

theorem spatialRight_mem_generated
    (hK : PublishedKaplanskyDensity.{u})
    (B : StarSubalgebra ℂ (K →L[ℂ] K))
    (A : StarSubalgebra ℂ (SpatialHilbert H K →L[ℂ] SpatialHilbert H K))
    (hBA : ∀ b ∈ B, spatialRight (H := H) b ∈ A)
…

Mentions: OAI.KadisonKastler.spatialRight

theorem OAI.KadisonKastler.generated_spatialMatrixAlgebra_eq_product line 70
Source documentation
The increasing finite spatial images generate the actual spatial product with the von Neumann algebra generated by the right stages.
```
theorem generated_spatialMatrixAlgebra_eq_product
    (hK : PublishedKaplanskyDensity.{u})
    (hE : Monotone (fun n => (E n).algebra)) :
    generatedVonNeumannAlgebra (⨆ n, spatialMatrixAlgebra M (E n)) =
      spatialProductAlgebra M (generatedVonNeumannAlgebra (⨆ n, (E n).algebra)) := by
…
```
Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.spatialMatrixAlgebra, OAI.KadisonKastler.spatialProductAlgebra

theorem OAI.KadisonKastler.exists_spatialMatrix_of_stage_union line 104

Source documentation

Every contraction test in the increasing union has an exact contractive matrix representative at a finite stage.

theorem exists_spatialMatrix_of_stage_union [Nontrivial K]
    (hs : ∀ n, 0 < s n) (hE : Monotone (fun n => (E n).algebra))
    {T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K}
    (hT : T ∈ (⨆ n, spatialMatrixAlgebra M (E n) :
      StarSubalgebra ℂ (SpatialHilbert H K →L[ℂ] SpatialHilbert H K))) (hn : ‖T‖ ≤ 1) :
    ∃ n, ∃ X : CStarMatrix (Fin (s n)) (Fin (s n)) (H →L[ℂ] H),
      (∀ i j, X i j ∈ M) ∧ ‖X‖ ≤ 1 ∧ spatialMatrixHom (E n) X = T := by
…

Mentions: OAI.KadisonKastler.spatialMatrixAlgebra, OAI.KadisonKastler.spatialMatrixHom

theorem OAI.KadisonKastler.spatialMatrix_union_weakUnitBallDense line 124

Source documentation

These explicit finite-image contraction tests are weakly dense in the unit ball of the spatial product.

theorem spatialMatrix_union_weakUnitBallDense
    (hK : PublishedKaplanskyDensity.{u})
    (hE : Monotone (fun n => (E n).algebra)) :
    WeakUnitBallDense
      (fun a : {a : ↥(⨆ n, spatialMatrixAlgebra M (E n)) // ‖a‖ ≤ 1} =>
        (a.val : SpatialHilbert H K →L[ℂ] SpatialHilbert H K))
      (spatialProductAlgebra M (generatedVonNeumannAlgebra (⨆ n, (E n).algebra))) := by
…

Mentions: OAI.KadisonKastler.WeakUnitBallDense, OAI.KadisonKastler.spatialMatrixAlgebra, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.generatedVonNeumannAlgebra