OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathPieces.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Each edge of an odd-subdivision round is an explicitly indexed piece of one previous route. Interior points of distinct pieces cannot coincide.

  1. def OAI.ContinuumCoulomb.QMAPathSchedule.nextParent line 14
  2. def OAI.ContinuumCoulomb.QMAPathSchedule.nextIndex line 19
  3. theorem OAI.ContinuumCoulomb.QMAPathSchedule.retained_work_zero line 25
  4. theorem OAI.ContinuumCoulomb.QMAPathSchedule.selected_work_pos line 31
  5. theorem OAI.ContinuumCoulomb.QMAPathSchedule.nextIndex_bounds line 35
  6. theorem OAI.ContinuumCoulomb.QMAPathSchedule.nextIndex_injective line 47
  7. theorem OAI.ContinuumCoulomb.QMAPathSchedule.nextIndex_interior line 56
  8. theorem OAI.ContinuumCoulomb.QMAPathSchedule.nextIndex_step line 67
  9. theorem OAI.ContinuumCoulomb.QMAPathSchedule.selectedIndex_injective line 78
  10. theorem OAI.ContinuumCoulomb.QMAPathSchedule.nextIndex_separated line 84