OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial coefficient program for both parities of a path gadget.

  1. abbrev OAI.ContinuumCoulomb.QuantumPathCode.Input line 12
  2. def OAI.ContinuumCoulomb.QuantumPathCode.inputCode line 13
  3. opaque OAI.ContinuumCoulomb.QuantumPathCode.evenProgram line 14
  4. opaque OAI.ContinuumCoulomb.QuantumPathCode.tailProgram line 15
  5. opaque OAI.ContinuumCoulomb.QuantumPathCode.radiusProgram line 16
  6. opaque OAI.ContinuumCoulomb.QuantumPathCode.weightProgram line 18
  7. opaque OAI.ContinuumCoulomb.QuantumPathCode.spokeProgram line 20
  8. opaque OAI.ContinuumCoulomb.QuantumPathCode.offsetProgram line 25
  9. def OAI.ContinuumCoulomb.QuantumPathCode.coefficients line 32
  10. opaque OAI.ContinuumCoulomb.QuantumPathCode.coefficientProgram line 36
  11. opaque OAI.ContinuumCoulomb.QuantumPathCode.coefficientListProgram line 50
  12. def OAI.ContinuumCoulomb.QuantumPathCode.coefficientListCertificate line 54
  13. theorem OAI.ContinuumCoulomb.QuantumPathCode.coefficients_spoke line 57
  14. theorem OAI.ContinuumCoulomb.QuantumPathCode.coefficients_offset line 62