OAI/Analysis/KadisonKastler/HilbertSumCorners.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The reducing coordinate corners of a Hilbert sum

  1. def OAI.KadisonKastler.hilbertSumInclusion line 18
  2. theorem OAI.KadisonKastler.hilbertSumInclusion_apply line 23
  3. theorem OAI.KadisonKastler.hilbertSumInclusion_adjoint_apply line 26
  4. abbrev OAI.KadisonKastler.hilbertSumProjection line 33
  5. theorem OAI.KadisonKastler.hilbertSumProjection_apply line 36
  6. theorem OAI.KadisonKastler.hilbertSumInclusion_extension_apply line 41
  7. def OAI.KadisonKastler.hilbertSumCompression line 46
  8. theorem OAI.KadisonKastler.hilbertSumCompression_apply line 49
  9. theorem OAI.KadisonKastler.hilbertSumCompression_norm_le line 53
  10. theorem OAI.KadisonKastler.hilbertSumCompression_extension line 61
  11. theorem OAI.KadisonKastler.hilbertSum_diagonal_of_commutes line 67
  12. theorem OAI.KadisonKastler.hilbertSumCompression_mem_corner line 74
  13. theorem OAI.KadisonKastler.hilbertSum_corner_commutes line 80