OAI/MathematicalPhysics/ContinuumCoulomb/Programs/FiniteDifferenceProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Literal rational programs for the three fixed coordinate differences. Their scalar sampler is supplied as a concrete Procedure, and is evaluated only a fixed number of times per gradient or Laplacian sample.

  1. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.shiftProgram line 14
  2. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.plusArgumentProgram line 42
  3. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.minusArgumentProgram line 48
  4. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.plusSampleProgram line 54
  5. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.minusSampleProgram line 60
  6. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.firstProgram line 66
  7. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.secondNumeratorProgram line 74
  8. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.stepSquareProgram line 85
  9. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.secondProgram line 90
  10. opaque OAI.ContinuumCoulomb.FiniteDifferenceProgram.laplacianProgram line 98