OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListSpatialPackage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Package the literal full fork graph with deterministic midpoint anchors. The package keeps its actual spin indices, coefficients and scalar offset.

  1. def OAI.ContinuumCoulomb.QuantumForkList.fullList line 15
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.fullList_bounded line 17
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.fullList_noLoops line 24
  4. def OAI.ContinuumCoulomb.QuantumForkList.fullGraph line 31
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.fullGraph_matrix line 36
  6. def OAI.ContinuumCoulomb.QuantumForkList.CommonCell line 44
  7. theorem OAI.ContinuumCoulomb.QuantumForkList.commonCell_refl line 47
  8. def OAI.ContinuumCoulomb.QuantumForkList.spatialModel line 50
  9. theorem OAI.ContinuumCoulomb.QuantumForkList.spatialModel_matrix line 76