OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitPhase.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A diagonal unitary rotates any chosen mediator X couplings to Y.

  1. def OAI.ContinuumCoulomb.qmaPhaseFactor line 15
  2. theorem OAI.ContinuumCoulomb.qmaPhaseFactor_gram line 18
  3. theorem OAI.ContinuumCoulomb.qmaPhaseFactor_flip line 22
  4. def OAI.ContinuumCoulomb.qmaAncillaPhase line 27
  5. theorem OAI.ContinuumCoulomb.qmaAncillaPhase_gram line 30
  6. def OAI.ContinuumCoulomb.qmaPhaseMatrix line 34
  7. theorem OAI.ContinuumCoulomb.qmaPhaseMatrix_gram line 37
  8. theorem OAI.ContinuumCoulomb.qmaPhaseMatrix_cogram line 45
  9. theorem OAI.ContinuumCoulomb.qmaAncillaPhase_flip line 53
  10. def OAI.ContinuumCoulomb.qmaPolarizedFlip line 65
  11. theorem OAI.ContinuumCoulomb.qmaDiagonal_sandwich line 69
  12. theorem OAI.ContinuumCoulomb.qmaPhaseMatrix_flip line 74
  13. theorem OAI.ContinuumCoulomb.qmaPhaseMatrix_diagonal line 84