OAI/MathematicalPhysics/ContinuumCoulomb/Programs/RawDensitySampleProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Literal arithmetic and TM2 compilation of the raw localized density sampler. The coordinate radius and requested accuracy are encoded unary.

  1. def OAI.ContinuumCoulomb.RawDensitySample.inputCode line 11
  2. opaque OAI.ContinuumCoulomb.RawDensitySample.paramsProgram line 14
  3. opaque OAI.ContinuumCoulomb.RawDensitySample.radiusProgram line 17
  4. opaque OAI.ContinuumCoulomb.RawDensitySample.precisionProgram line 20
  5. opaque OAI.ContinuumCoulomb.RawDensitySample.coordinatesProgram line 23
  6. opaque OAI.ContinuumCoulomb.RawDensitySample.firstCoordinateProgram line 26
  7. opaque OAI.ContinuumCoulomb.RawDensitySample.remainingCoordinatesProgram line 29
  8. opaque OAI.ContinuumCoulomb.RawDensitySample.secondCoordinateProgram line 33
  9. opaque OAI.ContinuumCoulomb.RawDensitySample.thirdCoordinateProgram line 36
  10. opaque OAI.ContinuumCoulomb.RawDensitySample.planarArgumentProgram line 39
  11. opaque OAI.ContinuumCoulomb.RawDensitySample.verticalArgumentProgram line 45
  12. opaque OAI.ContinuumCoulomb.RawDensitySample.program line 49
  13. def OAI.ContinuumCoulomb.RawDensitySample.certificate line 55