OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListSites.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual fork sites obtained from the ordered port arrays. Their bounds and injectivity are the geometric hypotheses of the parallel perturbation theorem.

  1. structure OAI.ContinuumCoulomb.QuantumForkList.ValidPorts line 12
  2. def OAI.ContinuumCoulomb.QuantumForkList.localPair line 23
  3. def OAI.ContinuumCoulomb.QuantumForkList.localFirst line 26
  4. def OAI.ContinuumCoulomb.QuantumForkList.localSecond line 30
  5. def OAI.ContinuumCoulomb.QuantumForkList.actualSite line 34
  6. def OAI.ContinuumCoulomb.QuantumForkList.actualJ line 42
  7. def OAI.ContinuumCoulomb.QuantumForkList.actualK line 45
  8. theorem OAI.ContinuumCoulomb.QuantumForkList.actualSite_injective line 48
  9. theorem OAI.ContinuumCoulomb.QuantumForkList.catalog_actualSite line 66