OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCellRouteSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A catalog path stays in the cells of its two endpoints. This transfers positivity and box bounds from physical spins to all subdivision sites.

  1. theorem OAI.ContinuumCoulomb.qmaLocalPort_bounded line 10
  2. theorem OAI.ContinuumCoulomb.qmaPointCell_localPort line 14
  3. theorem OAI.ContinuumCoulomb.qmaPointCell_halfPath line 18
  4. theorem OAI.ContinuumCoulomb.qmaPointCell_internalPath line 23
  5. theorem OAI.ContinuumCoulomb.QMACellRouteBody.path_cells line 31
  6. theorem OAI.ContinuumCoulomb.QMACellRoute.path_cells line 46
  7. theorem OAI.ContinuumCoulomb.QMACellRoute.path_positive line 54
  8. theorem OAI.ContinuumCoulomb.QMACellRoute.path_bounded line 65