OAI/InformationTheory/Entanglement/ProjectionSquare.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProjectionCriterion.hsAdjoint_left_ad line 11
  2. def OAI.ProjectionCriterion.Data.firstCoordinates line 30
  3. def OAI.ProjectionCriterion.Data.Xi1 line 32
  4. def OAI.ProjectionCriterion.Data.Xi2 line 33
  5. lemma OAI.ProjectionCriterion.Data.Xi1_ppt line 36
  6. lemma OAI.ProjectionCriterion.Data.Xi2_ppt line 38
  7. lemma OAI.ProjectionCriterion.Data.Xi2_adjoint line 40
  8. lemma OAI.ProjectionCriterion.Data.Xi_composite line 42
  9. lemma OAI.ProjectionCriterion.Data.Xi_not_eb line 54
  10. theorem OAI.ProjectionCriterion.square_embedding line 61