OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRebitSoundness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Realification preserves lower quadratic bounds on all complex vectors, not only on the real-coordinate encoding of a witness.

  1. def OAI.ContinuumCoulomb.qmaRealVector line 13
  2. def OAI.ContinuumCoulomb.qmaImagVector line 15
  3. theorem OAI.ContinuumCoulomb.qmaQuadratic_real_split line 17
  4. def OAI.ContinuumCoulomb.qmaUnrebitReal line 24
  5. def OAI.ContinuumCoulomb.qmaUnrebitImag line 27
  6. theorem OAI.ContinuumCoulomb.qmaRebitVector_unrebitReal line 30
  7. theorem OAI.ContinuumCoulomb.qmaRebitVector_unrebitImag line 36
  8. theorem OAI.ContinuumCoulomb.qmaRebitMatrix_quadratic_split line 42
  9. theorem OAI.ContinuumCoulomb.qmaRebitVector_mass_split line 50
  10. theorem OAI.ContinuumCoulomb.qmaRebitMatrix_lower line 57