OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListScale.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact rational calibration for the ordered fork list. The perturbation scale includes the unpaired active ports in its retained-energy bound.

  1. def OAI.ContinuumCoulomb.QuantumForkList.countProgram line 13
  2. def OAI.ContinuumCoulomb.QuantumForkList.bondsProgram line 15
  3. def OAI.ContinuumCoulomb.QuantumForkList.scalarProgram line 21
  4. def OAI.ContinuumCoulomb.QuantumForkList.groupsProgram line 27
  5. def OAI.ContinuumCoulomb.QuantumForkList.leftWeight line 33
  6. def OAI.ContinuumCoulomb.QuantumForkList.rightWeight line 35
  7. def OAI.ContinuumCoulomb.QuantumForkList.pairLinearProgram line 38
  8. def OAI.ContinuumCoulomb.QuantumForkList.pairSquareProgram line 46
  9. def OAI.ContinuumCoulomb.QuantumForkList.pairOffsetProgram line 52
  10. abbrev OAI.ContinuumCoulomb.QuantumForkList.ScaleInput line 60
  11. def OAI.ContinuumCoulomb.QuantumForkList.scaleCode line 61
  12. def OAI.ContinuumCoulomb.QuantumForkList.scaleProgram line 63