OAI/Analysis/KadisonKastler/MatrixCorners.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.matrixCorner line 13
2. theorem OAI.KadisonKastler.matrixCorner_injective line 17
3. theorem OAI.KadisonKastler.matrixCorner_zero line 23
4. theorem OAI.KadisonKastler.matrixCorner_mul line 27
5. theorem OAI.KadisonKastler.matrixCorner_star line 32
6. theorem OAI.KadisonKastler.matrixCorner_isStarProjection_iff line 37
7. theorem OAI.KadisonKastler.matrixCorner_reconstruct line 53
8. theorem OAI.KadisonKastler.matrixCorner_diffuse line 67

   Source documentation

   A diagonal corner inherits exactly the projection-splitting property of the original algebra.

   theorem matrixCorner_diffuse
       (hdiff : ∀ p : B, IsStarProjection p → p ≠ 0 →
         ∃ q : B, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
       (i : ι) (p : CStarMatrix ι ι B) (hp : IsStarProjection p) (hp0 : p ≠ 0)
       (hleft : matrixCorner i 1 * p = p) (hright : p * matrixCorner i 1 = p) :
       ∃ q : CStarMatrix ι ι B, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧
         p * q = q ∧ q * p = q := by
   …

   Mentions: OAI.KadisonKastler.matrixCorner