OAI/Analysis/KadisonKastler/ProjectionFamilyCorner.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The remaining corner inside a family pinching

The quadratic remainder projection is contained in the simultaneous commutation projection, including for infinite projection families.

  1. theorem OAI.KadisonKastler.projectionFamily_left_annihilate line 20
  2. theorem OAI.KadisonKastler.projectionFamily_right_annihilate line 26
  3. theorem OAI.KadisonKastler.orthogonal_modularQuadratic_annihilate line 34
  4. theorem OAI.KadisonKastler.projectionFamily_quadratic_mem_commutation line 49
  5. theorem OAI.KadisonKastler.projectionFamilyPinching_quadratic line 62
  6. theorem OAI.KadisonKastler.projectionFamilyCommutationSpace_conjugate line 72
  7. theorem OAI.KadisonKastler.projectionFamily_remainder_central line 86
  8. theorem OAI.KadisonKastler.projectionFamily_remainder_mul_pinching line 124