OAI/Analysis/KadisonKastler/MatrixLiftBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.matrixUnitsEmbedding_map line 21
2. def OAI.KadisonKastler.finiteMatrixAmbientEmbedding line 32

   Source documentation

   The coordinate finite model, now viewed directly as a matrix of operators on the original Hilbert space.

   def finiteMatrixAmbientEmbedding (E : Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M)) :
       FiniteMatrixModel n j →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H) :=
   …

   Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteMatrixModel

3. theorem OAI.KadisonKastler.mappedMatrixUnits_algebra_le line 36
4. theorem OAI.KadisonKastler.finiteMatrixAmbientEmbedding_entry_mem line 46
5. theorem OAI.KadisonKastler.finiteMatrix_unitary_commutator_le line 58

   Source documentation

   Every coordinate finite-matrix unitary has commutator bounded by twice the scalar derivation bound, uniformly in both matrix sizes.

   theorem finiteMatrix_unitary_commutator_le
       (E : Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M))
       (h : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
       (hb : ∀ a ∈ M, ‖h * a - a * h‖ ≤ δ * ‖a‖)
       (u : unitary (FiniteMatrixModel n j)) :
       let v := Unitary.map (StarMonoidHom.ofClass (finiteMatrixAmbientEmbedding E)) u
   …

   Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.finiteMatrixAmbientEmbedding