OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedHistory.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reordering actual history terms preserves the full-space reference gap.

  1. def OAI.ContinuumCoulomb.qmaOrderedReferenceTerms line 12
  2. theorem OAI.ContinuumCoulomb.qmaOrderedReferenceTerms_sum line 17
  3. def OAI.ContinuumCoulomb.qmaOrderedReferenceHistory line 23
  4. theorem OAI.ContinuumCoulomb.qmaOrderedReferenceHistory_lower line 28
  5. theorem OAI.ContinuumCoulomb.qmaOrderedReferenceHistory_accepting line 48