OAI/InformationTheory/Entanglement/CombinatorialMain.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProjectionCriterion.Data.real_reindex line 20
  2. lemma OAI.FiniteConstruction.Q_pos line 27
  3. lemma OAI.FiniteConstruction.D_pos line 28
  4. instance OAI.FiniteConstruction.questionNonempty line 29
  5. instance OAI.FiniteConstruction.dNeZero line 31
  6. lemma OAI.FiniteConstruction.D_le_m line 32
  7. def OAI.FiniteConstruction.concreteData line 36
  8. lemma OAI.FiniteConstruction.data_real line 38
  9. lemma OAI.FiniteConstruction.concrete_real line 44
  10. def OAI.FiniteConstruction.Psi line 47
  11. def OAI.FiniteConstruction.Lambda line 48
  12. def OAI.FiniteConstruction.localChannel line 49
  13. def OAI.FiniteConstruction.rho line 50
  14. def OAI.FiniteConstruction.Phi1 line 51
  15. def OAI.FiniteConstruction.Phi2 line 52
  16. def OAI.FiniteConstruction.Theta line 53
  17. lemma OAI.FiniteConstruction.localChannel_exact line 55
  18. lemma OAI.FiniteConstruction.rho_exact line 58
  19. lemma OAI.FiniteConstruction.Phi1_ppt line 62
  20. lemma OAI.FiniteConstruction.Phi2_ppt line 63
  21. lemma OAI.FiniteConstruction.pair_identification line 64
  22. lemma OAI.FiniteConstruction.composite_nonseparable line 70
  23. lemma OAI.FiniteConstruction.pair_not_eb line 74
  24. lemma OAI.FiniteConstruction.theta_ppt line 75
  25. lemma OAI.FiniteConstruction.theta_tp line 76
  26. lemma OAI.FiniteConstruction.theta_corner line 77
  27. lemma OAI.FiniteConstruction.theta_not_eb line 81
  28. theorem OAI.FiniteConstruction.combinatorial_algebraic_clauses line 84