OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumInflatedPath.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Replace each unit edge of a simple path by its eight-step corridor.

  1. def OAI.ContinuumCoulomb.qmaInflatedPoint line 9
  2. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_zero line 12
  3. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_boundary line 15
  4. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_last line 19
  5. theorem OAI.ContinuumCoulomb.qmaLeafCenter_injective line 23
  6. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_step line 29
  7. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_gridline line 53
  8. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_not_center line 64
  9. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_injective line 77