OAI/Analysis/KadisonKastler/ProjectionFamilyMaximal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Maximal admissible orthogonal projection families

Chain unions retain the two quantitative inequalities by strong convergence of the constructed kernel projections.

  1. def OAI.KadisonKastler.AdmissibleOrthogonalFamily line 21
  2. theorem OAI.KadisonKastler.projectionFamilyRemainder_empty line 26
  3. theorem OAI.KadisonKastler.projectionFamilyPinching_empty line 35
  4. theorem OAI.KadisonKastler.admissibleOrthogonalFamily_empty line 43
  5. theorem OAI.KadisonKastler.exists_maximal_admissibleOrthogonalFamily line 50