OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRouteLeafProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial TM2 evaluators for scaled centers and reserved leaves.

  1. def OAI.ContinuumCoulomb.QuantumRouteLeafCode.coordinateProgram line 15
  2. opaque OAI.ContinuumCoulomb.QuantumRouteLeafCode.centerProgram line 25
  3. def OAI.ContinuumCoulomb.QuantumRouteLeafCode.leafProgram line 28
  4. opaque OAI.ContinuumCoulomb.QuantumRouteLeafCode.leafListProgram line 42
  5. abbrev OAI.ContinuumCoulomb.QuantumRouteLeafCode.Ends line 46
  6. def OAI.ContinuumCoulomb.QuantumRouteLeafCode.endsCode line 47
  7. opaque OAI.ContinuumCoulomb.QuantumRouteLeafCode.firstProgram line 48
  8. opaque OAI.ContinuumCoulomb.QuantumRouteLeafCode.secondProgram line 49
  9. def OAI.ContinuumCoulomb.QuantumRouteLeafCode.axisProgram line 50
  10. opaque OAI.ContinuumCoulomb.QuantumRouteLeafCode.directionProgram line 62
  11. opaque OAI.ContinuumCoulomb.QuantumRouteLeafCode.selectedLeafProgram line 77
  12. def OAI.ContinuumCoulomb.QuantumRouteLeafCode.centerCertificate line 90
  13. def OAI.ContinuumCoulomb.QuantumRouteLeafCode.selectedLeafCertificate line 92