OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumReferenceLower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive local history terms make a constant-strength reference penalty sufficient.

  1. theorem OAI.ContinuumCoulomb.qmaQuadratic_sum line 14
  2. theorem OAI.ContinuumCoulomb.qmaQuadratic_identity line 23
  3. theorem OAI.ContinuumCoulomb.qmaReferenceSector_nonnegative line 28
  4. theorem OAI.ContinuumCoulomb.qmaReferenceSector_lower line 40