OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedTwoStage.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The literal rational six-to-four-to-three-local compiler. Every intermediate word retains its ordered site list, and the estimate compares the ordinary full Hilbert-space ground energies.

  1. def OAI.ContinuumCoulomb.QuantumOrderedTwoStage.firstWord line 15
  2. def OAI.ContinuumCoulomb.QuantumOrderedTwoStage.firstSites line 16
  3. def OAI.ContinuumCoulomb.QuantumOrderedTwoStage.firstCoefficient line 17
  4. def OAI.ContinuumCoulomb.QuantumOrderedTwoStage.word line 19
  5. def OAI.ContinuumCoulomb.QuantumOrderedTwoStage.sites line 22
  6. def OAI.ContinuumCoulomb.QuantumOrderedTwoStage.coefficient line 24
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedTwoStage.sites_nodup line 28
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedTwoStage.sites_length line 33
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedTwoStage.support_cover line 39
  10. theorem OAI.ContinuumCoulomb.QuantumOrderedTwoStage.support line 43
  11. theorem OAI.ContinuumCoulomb.QuantumOrderedTwoStage.even line 49
  12. theorem OAI.ContinuumCoulomb.QuantumOrderedTwoStage.accuracy line 57