OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumReferenceBasis.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A local Y-eigenbasis for distributing the realification reference qubit.

  1. def OAI.ContinuumCoulomb.qmaReferencePhase line 13
  2. def OAI.ContinuumCoulomb.qmaReferenceBasis line 15
  3. def OAI.ContinuumCoulomb.qmaImaginaryRotation line 17
  4. theorem OAI.ContinuumCoulomb.qmaReferencePhase_gram line 19
  5. theorem OAI.ContinuumCoulomb.qmaReferenceBasis_gram line 24
  6. theorem OAI.ContinuumCoulomb.qmaReferenceBasis_y line 28
  7. theorem OAI.ContinuumCoulomb.qmaImaginaryRotation_eq line 52
  8. theorem OAI.ContinuumCoulomb.qmaReferenceBasis_rotation line 56
  9. def OAI.ContinuumCoulomb.qmaEntryReal line 61
  10. def OAI.ContinuumCoulomb.qmaEntryImag line 64
  11. theorem OAI.ContinuumCoulomb.qmaRebitMatrix_tensor line 67