OAI/MathematicalPhysics/ContinuumCoulomb/Programs/TransformedGaussProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A literal polynomial TM2 program for the transported rational Gauss node. The reciprocal mesh denominator and lattice coordinates are binary; the requested reciprocal error bound is unary.

  1. abbrev OAI.ContinuumCoulomb.TransformedGauss.Input line 15
  2. def OAI.ContinuumCoulomb.TransformedGauss.inputCode line 16
  3. def OAI.ContinuumCoulomb.TransformedGauss.output line 21
  4. opaque OAI.ContinuumCoulomb.TransformedGauss.precisionProgram line 24
  5. opaque OAI.ContinuumCoulomb.TransformedGauss.inputParametersProgram line 29
  6. opaque OAI.ContinuumCoulomb.TransformedGauss.dataProgram line 31
  7. opaque OAI.ContinuumCoulomb.TransformedGauss.inputPrecisionProgram line 35
  8. opaque OAI.ContinuumCoulomb.TransformedGauss.denominatorProgram line 38
  9. opaque OAI.ContinuumCoulomb.TransformedGauss.fieldParametersProgram line 40
  10. opaque OAI.ContinuumCoulomb.TransformedGauss.tailProgram line 42
  11. opaque OAI.ContinuumCoulomb.TransformedGauss.sitesProgram line 45
  12. opaque OAI.ContinuumCoulomb.TransformedGauss.nodeDataProgram line 47
  13. opaque OAI.ContinuumCoulomb.TransformedGauss.nodeArgumentsProgram line 50
  14. opaque OAI.ContinuumCoulomb.TransformedGauss.initialNodeProgram line 53
  15. opaque OAI.ContinuumCoulomb.TransformedGauss.flowArgumentsProgram line 56
  16. opaque OAI.ContinuumCoulomb.TransformedGauss.program line 62
  17. def OAI.ContinuumCoulomb.TransformedGauss.certificate line 66