OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListGraph.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite bond packet emitted for parallel forks has the exact full-space Hamiltonian used in the calibrated perturbation estimate.

  1. def OAI.ContinuumCoulomb.QuantumForkList.packetBonds line 13
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.packetBonds_matrix line 18
  3. def OAI.ContinuumCoulomb.QuantumForkList.graphBonds line 32
  4. def OAI.ContinuumCoulomb.QuantumForkList.graphConstant line 38
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.graph_matrix line 41
  6. def OAI.ContinuumCoulomb.QuantumForkList.graphScale line 58
  7. theorem OAI.ContinuumCoulomb.QuantumForkList.graphScale_cast line 64
  8. theorem OAI.ContinuumCoulomb.QuantumForkList.graph_accuracy line 73