OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGridWalk.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A finite unit-step route has a simple subroute with no larger length.

  1. def OAI.ContinuumCoulomb.qmaSquareGrid line 10
  2. theorem OAI.ContinuumCoulomb.qmaManhattanPoint_adj line 15
  3. def OAI.ContinuumCoulomb.qmaGridWalk line 20
  4. theorem OAI.ContinuumCoulomb.qmaGridWalk_length line 28
  5. theorem OAI.ContinuumCoulomb.qmaGridWalk_support line 35
  6. def OAI.ContinuumCoulomb.qmaSimpleGridPath line 49
  7. theorem OAI.ContinuumCoulomb.qmaSimpleGridPath_length line 53
  8. theorem OAI.ContinuumCoulomb.qmaSimpleGridPath_support line 58
  9. theorem OAI.ContinuumCoulomb.qmaGridPath_getVert_step line 64