OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRouteLeaf.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Reserve one singlet leaf beside the initial step of every scaled route. Four incident directions use four different quadrants.

  1. def OAI.ContinuumCoulomb.qmaLeafCenter line 10
  2. def OAI.ContinuumCoulomb.qmaLeafFirst line 12
  3. def OAI.ContinuumCoulomb.qmaRouteLeaf line 16
  4. theorem OAI.ContinuumCoulomb.qmaLeafFirst_step line 20
  5. theorem OAI.ContinuumCoulomb.qmaRouteLeaf_step line 24
  6. theorem OAI.ContinuumCoulomb.qmaRouteLeaf_cell line 28
  7. theorem OAI.ContinuumCoulomb.qmaRouteLeaf_not_gridline line 32
  8. theorem OAI.ContinuumCoulomb.qmaRouteLeaf_avoids line 36
  9. theorem OAI.ContinuumCoulomb.qmaRouteLeaf_injective line 43
  10. theorem OAI.ContinuumCoulomb.qmaRouteLeaf_bounds line 57