OAI/MathematicalPhysics/ContinuumCoulomb/Programs/GaussianPacketProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The fixed-frequency Gaussian sample has an actual polynomial-time Turing program. Both its frequency computation and its exponential computation use explicit polynomial unary precision schedules.

  1. def OAI.ContinuumCoulomb.GaussianPacket.inputCode line 12
  2. opaque OAI.ContinuumCoulomb.GaussianPacket.radiusProgram line 14
  3. opaque OAI.ContinuumCoulomb.GaussianPacket.precisionProgram line 18
  4. opaque OAI.ContinuumCoulomb.GaussianPacket.pointProgram line 22
  5. opaque OAI.ContinuumCoulomb.GaussianPacket.radiusSquareProgram line 25
  6. opaque OAI.ContinuumCoulomb.GaussianPacket.frequencyPrecisionProgram line 28
  7. opaque OAI.ContinuumCoulomb.GaussianPacket.frequencyProgram line 36
  8. opaque OAI.ContinuumCoulomb.GaussianPacket.exponentProgram line 40
  9. opaque OAI.ContinuumCoulomb.GaussianPacket.magnitudeProgram line 46
  10. opaque OAI.ContinuumCoulomb.GaussianPacket.exponentialPrecisionProgram line 52
  11. opaque OAI.ContinuumCoulomb.GaussianPacket.argumentProgram line 58
  12. opaque OAI.ContinuumCoulomb.GaussianPacket.program line 62
  13. def OAI.ContinuumCoulomb.GaussianPacket.certificate line 66