OAI/Analysis/KadisonKastler/SpatialMatrixImage.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.MatrixNearInclusion.spatialMatrix_approx line 29

   Source documentation

   Matrix proximity gives an actual finite spatial image approximant.

   theorem MatrixNearInclusion.spatialMatrix_approx
       {M N : VonNeumannAlgebra H} {γ : ℝ} (h : MatrixNearInclusion M N γ)
       [Nonempty ι] [Nontrivial K] (E : MatrixUnitSystem ι (K →L[ℂ] K))
       (X : CStarMatrix ι ι (H →L[ℂ] H)) (hX : ∀ i j, X i j ∈ M) (hn : ‖X‖ ≤ 1) :
       ∃ Y : CStarMatrix ι ι (H →L[ℂ] H), (∀ i j, Y i j ∈ N) ∧ ‖Y‖ ≤ 1 ∧
         ‖spatialMatrixHom E X - spatialMatrixHom E Y‖ ≤ γ := by
   …

   Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.spatialMatrixHom

2. def OAI.KadisonKastler.spatialMatrixAlgebraHom line 41

   Source documentation

   The finite matrix image with coefficients restricted to M.

   def spatialMatrixAlgebraHom (M : VonNeumannAlgebra H)
       (E : MatrixUnitSystem ι (K →L[ℂ] K)) :
       CStarMatrix ι ι (Algebra M) →⋆ₐ[ℂ]
         (SpatialHilbert H K →L[ℂ] SpatialHilbert H K) :=
   …

   Mentions: OAI.KadisonKastler.Algebra

3. def OAI.KadisonKastler.spatialMatrixAlgebra line 47
4. theorem OAI.KadisonKastler.spatialMatrixAlgebraHom_apply line 52
5. theorem OAI.KadisonKastler.spatialTensorOp_sum_right line 59
6. theorem OAI.KadisonKastler.spatialLeft_mem_matrixAlgebra line 67
7. theorem OAI.KadisonKastler.spatialRight_mem_matrixAlgebra line 95
8. theorem OAI.KadisonKastler.spatialMatrixAlgebra_eq_sup line 110

   Source documentation

   The finite image is exactly the star algebra generated by the two commuting coefficient algebras.

   theorem spatialMatrixAlgebra_eq_sup (M : VonNeumannAlgebra H)
       (E : MatrixUnitSystem ι (K →L[ℂ] K)) :
       spatialMatrixAlgebra M E =
         M.toStarSubalgebra.map (spatialLeft (K := K)) ⊔
   …

   Mentions: OAI.KadisonKastler.spatialMatrixAlgebra, OAI.KadisonKastler.spatialLeft

9. theorem OAI.KadisonKastler.spatialMatrixAlgebra_mono line 142
10. theorem OAI.KadisonKastler.spatialMatrixAlgebra_le_product line 149
11. theorem OAI.KadisonKastler.exists_matrix_of_mem_spatialMatrixAlgebra line 158

    Source documentation

    Every contraction in the finite image has an exact contractive operator-valued matrix representative.

    theorem exists_matrix_of_mem_spatialMatrixAlgebra
        [Nonempty ι] [Nontrivial K]
        (M : VonNeumannAlgebra H) (E : MatrixUnitSystem ι (K →L[ℂ] K))
        {T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K}
        (hT : T ∈ spatialMatrixAlgebra M E) (hn : ‖T‖ ≤ 1) :
        ∃ X : CStarMatrix ι ι (H →L[ℂ] H), (∀ i j, X i j ∈ M) ∧ ‖X‖ ≤ 1 ∧
          spatialMatrixHom E X = T := by
    …

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