OAI/Analysis/KadisonKastler/TwoStatePositiveTransport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Spatial transport determined by the positive two-state matrix vector

  1. abbrev OAI.KadisonKastler.twoStateQuadraticBridge line 16
  2. def OAI.KadisonKastler.twoStatePositiveTransport line 20
  3. theorem OAI.KadisonKastler.twoStateQuadraticBridge_triple line 26
  4. theorem OAI.KadisonKastler.twoStatePositiveTransport_embedding line 35
  5. theorem OAI.KadisonKastler.twoStatePositiveTransport_inverse_embedding line 47
  6. theorem OAI.KadisonKastler.twoStateQuadratic_projection_reference line 66
  7. theorem OAI.KadisonKastler.twoStatePositiveTransport_inverse_reference line 79
  8. def OAI.KadisonKastler.twoStateDiagonalEntry line 95
  9. theorem OAI.KadisonKastler.diagonal_fst line 99
  10. theorem OAI.KadisonKastler.diagonal_snd line 106
  11. theorem OAI.KadisonKastler.twoStateDiagonalEntry_corner line 113
  12. theorem OAI.KadisonKastler.diagonal_commutes_entry line 128
  13. theorem OAI.KadisonKastler.twoStateQuadraticBridge_commutes line 144
  14. theorem OAI.KadisonKastler.twoStatePositiveTransport_intertwines line 153