OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathEmbedding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Geometric invariants for the variable-length path-subdivision schedule.

  1. structure OAI.ContinuumCoulomb.QMAPathEmbedding line 13
  2. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.selected_work_pos line 29
  3. def OAI.ContinuumCoulomb.QMAPathEmbedding.freshPosition line 32
  4. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.freshPosition_ne_old line 35
  5. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.freshPosition_injective line 43
  6. def OAI.ContinuumCoulomb.QMAPathEmbedding.nextPosition line 64
  7. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.nextPosition_old line 67
  8. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.nextPosition_fresh line 70
  9. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.nextPosition_injective line 73
  10. theorem OAI.ContinuumCoulomb.QMAPathEmbedding.adjacent_of_complete line 89