OAI/Analysis/KadisonKastler/StrongUnitaryEvaluation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Evaluation on the strong-star Polish unitary model

  1. def OAI.KadisonKastler.encodeStrongUnitary line 16
  2. def OAI.KadisonKastler.decodeStrongUnitary line 19
  3. theorem OAI.KadisonKastler.unitaryCoordinates_decode line 22
  4. theorem OAI.KadisonKastler.decodeStrongUnitary_apply_test line 26
  5. theorem OAI.KadisonKastler.star_decodeStrongUnitary_apply_test line 30
  6. theorem OAI.KadisonKastler.decode_encodeStrongUnitary line 35
  7. theorem OAI.KadisonKastler.encode_decodeStrongUnitary line 40
  8. theorem OAI.KadisonKastler.decode_norm_le_one line 44
  9. theorem OAI.KadisonKastler.star_decode_norm_le_one line 50
  10. theorem OAI.KadisonKastler.continuous_decodeStrongUnitary_apply line 55
  11. theorem OAI.KadisonKastler.continuous_star_decodeStrongUnitary_apply line 72
  12. theorem OAI.KadisonKastler.continuous_decodeStrongUnitary_apply_joint line 90
  13. theorem OAI.KadisonKastler.continuous_star_decodeStrongUnitary_apply_joint line 103