OAI/Analysis/KadisonKastler/CentralDefectSelfAdjoint.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Reducing a central-vector defect to a self-adjoint contraction

  1. def OAI.KadisonKastler.centralVectorDefect line 14
  2. theorem OAI.KadisonKastler.centralVectorDefect_apply line 22
  3. theorem OAI.KadisonKastler.centralVectorDefect_star_norm line 25
  4. theorem OAI.KadisonKastler.centralVectorDefect_realPart_le line 35
  5. theorem OAI.KadisonKastler.centralVectorDefect_imaginaryPart_le line 47
  6. theorem OAI.KadisonKastler.centralVectorDefect_re_im_gap line 60