OAI/Analysis/KadisonKastler/FreeDiagonalBlockModel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.offDiagonal_eq line 15
2. theorem OAI.KadisonKastler.offDiagonal_blocks line 21
3. theorem OAI.KadisonKastler.offDiagonal_gram line 31
4. def OAI.KadisonKastler.freeDiagonalModel_of_leadingProjections line 56

   Source documentation

   The only geometric construction still needed is a family of orthogonal leading-word projections whose complementary centered blocks vanish.

   def freeDiagonalModel_of_leadingProjections
       (e : ι → α → H →L[ℂ] H)
       (he : ∀ i a, IsStarProjection (e i a))
       (heo : ∀ i a b, a ≠ b → e i a * e i b = 0)
       (hes : ∀ i, ∑ a, e i a = 1)
       (P : ι → H →L[ℂ] H) (hP : ∀ i, IsStarProjection (P i))
       (hPo : ∀ i j, i ≠ j → P i * P j = 0)
       (hblock : ∀ i a, (1 - P i) * diagonalCentered e i a * (1 - P i) = 0) :
       FreeDiagonalModel ι α H where
   …

   Mentions: OAI.KadisonKastler.diagonalCentered, OAI.KadisonKastler.FreeDiagonalModel