OAI/InformationTheory/Entanglement/MainStateAlgebra.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.sharp_ppt line 14
  2. lemma OAI.SecretKey.projector_real_smul line 17
  3. lemma OAI.SecretKey.psd_trace_re_pos line 24
  4. lemma OAI.SecretKey.psd_trace_ofReal line 35
  5. lemma OAI.SecretKey.normalized_psd line 41
  6. lemma OAI.SecretKey.normalized_trace line 45
  7. def OAI.ExplicitPencil.stateTrace line 54
  8. def OAI.ExplicitPencil.rho line 56
  9. def OAI.ExplicitPencil.stateVector line 58
  10. lemma OAI.ExplicitPencil.Z_psd line 60
  11. lemma OAI.ExplicitPencil.stateTrace_pos line 61
  12. lemma OAI.ExplicitPencil.rho_psd line 62
  13. lemma OAI.ExplicitPencil.rho_trace line 63
  14. lemma OAI.ExplicitPencil.rho_ne_zero line 64
  15. lemma OAI.ExplicitPencil.rho_no_product line 69
  16. lemma OAI.ExplicitPencil.rho_entangled line 76
  17. lemma OAI.ExplicitPencil.stateVector_projector line 80
  18. lemma OAI.ExplicitPencil.rho_identification line 83
  19. lemma OAI.ExplicitPencil.rho_represented line 86
  20. theorem OAI.ExplicitPencil.main_state_algebra line 92