OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCoordinateSpectrum.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The local qubit-coordinate matrices retain the full-space spectral bounds, through explicit basis equivalences.

  1. theorem OAI.ContinuumCoulomb.qmaQuadratic_reindex line 14
  2. theorem OAI.ContinuumCoulomb.qmaNorm_reindex line 24
  3. def OAI.ContinuumCoulomb.qmaRebitQubitSplit line 30
  4. def OAI.ContinuumCoulomb.qmaRealCircuitQubitSplit line 40
  5. def OAI.ContinuumCoulomb.qmaRealQubitHamiltonian line 45
  6. theorem OAI.ContinuumCoulomb.qmaRealQubitHamiltonian_reindex line 47
  7. theorem OAI.ContinuumCoulomb.qmaRealQubitHamiltonian_sound line 51
  8. theorem OAI.ContinuumCoulomb.qmaRealQubitHamiltonian_accepting line 67