OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRealification.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

One extra real qubit represents the real and imaginary coordinates of an arbitrary complex Hamiltonian without changing its quadratic energy.

  1. def OAI.ContinuumCoulomb.qmaRebitMatrix line 13
  2. def OAI.ContinuumCoulomb.qmaRebitVector line 17
  3. theorem OAI.ContinuumCoulomb.qmaRebitMatrix_real line 20
  4. theorem OAI.ContinuumCoulomb.qmaRebitMatrix_hermitian line 27
  5. theorem OAI.ContinuumCoulomb.qmaRebitVector_mass line 38
  6. theorem OAI.ContinuumCoulomb.qmaRebitVector_inner line 43
  7. theorem OAI.ContinuumCoulomb.qmaRebitMatrix_mulVec line 48
  8. theorem OAI.ContinuumCoulomb.qmaRebitMatrix_quadratic line 58