OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEvenListPieces.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Literal reserved-leaf and tail arrays for an even route subdivision.

  1. def OAI.ContinuumCoulomb.QuantumEvenListPieces.leaf line 12
  2. def OAI.ContinuumCoulomb.QuantumEvenListPieces.fresh line 16
  3. def OAI.ContinuumCoulomb.QuantumEvenListPieces.paths line 18
  4. opaque OAI.ContinuumCoulomb.QuantumEvenListPieces.leafProgram line 23
  5. def OAI.ContinuumCoulomb.QuantumEvenListPieces.pointProgram line 29
  6. def OAI.ContinuumCoulomb.QuantumEvenListPieces.pairList line 35
  7. opaque OAI.ContinuumCoulomb.QuantumEvenListPieces.freshProgram line 41
  8. opaque OAI.ContinuumCoulomb.QuantumEvenListPieces.pathsProgram line 44
  9. theorem OAI.ContinuumCoulomb.QuantumEvenListPieces.tail_reverse line 56
  10. theorem OAI.ContinuumCoulomb.QuantumEvenListPieces.leaf_range line 70
  11. theorem OAI.ContinuumCoulomb.QuantumEvenListPieces.fresh_range line 76
  12. theorem OAI.ContinuumCoulomb.QuantumEvenListPieces.paths_range line 82