OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitPhasePhysical.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Independent mediator phase rotations preserve the full physical spectrum.

  1. def OAI.ContinuumCoulomb.qmaPhaseLift line 14
  2. theorem OAI.ContinuumCoulomb.qmaPhaseLift_gram line 17
  3. theorem OAI.ContinuumCoulomb.qmaPhaseLift_cogram line 23
  4. theorem OAI.ContinuumCoulomb.qmaPhaseLift_sandwich line 29
  5. theorem OAI.ContinuumCoulomb.qmaPhaseLift_diagonal line 37
  6. theorem OAI.ContinuumCoulomb.qmaPhaseLift_old line 42
  7. theorem OAI.ContinuumCoulomb.qmaPhaseLift_flip line 47
  8. def OAI.ContinuumCoulomb.qmaPolarizedPhysical line 52
  9. theorem OAI.ContinuumCoulomb.qmaPhaseLift_physical line 57
  10. theorem OAI.ContinuumCoulomb.qmaPolarizedPhysical_bottom line 72