OAI/MathematicalPhysics/ContinuumCoulomb/Programs/CountertermProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial programs evaluate the exact counterterm formula with the error certified in CountertermEvaluation.

  1. abbrev OAI.ContinuumCoulomb.CountertermEvaluation.EntryInput line 13
  2. abbrev OAI.ContinuumCoulomb.CountertermEvaluation.RowInput line 14
  3. def OAI.ContinuumCoulomb.CountertermEvaluation.rowCode line 15
  4. opaque OAI.ContinuumCoulomb.CountertermEvaluation.maxOneProgram line 18
  5. opaque OAI.ContinuumCoulomb.CountertermEvaluation.onsiteArgumentProgram line 29
  6. opaque OAI.ContinuumCoulomb.CountertermEvaluation.onsiteProgram line 36
  7. opaque OAI.ContinuumCoulomb.CountertermEvaluation.guardProgram line 40
  8. opaque OAI.ContinuumCoulomb.CountertermEvaluation.scaledOnsiteProgram line 43
  9. opaque OAI.ContinuumCoulomb.CountertermEvaluation.denominatorProgram line 47
  10. opaque OAI.ContinuumCoulomb.CountertermEvaluation.entryNumeratorProgram line 50
  11. opaque OAI.ContinuumCoulomb.CountertermEvaluation.entryDenominatorProgram line 55
  12. opaque OAI.ContinuumCoulomb.CountertermEvaluation.entryArgumentsProgram line 59
  13. opaque OAI.ContinuumCoulomb.CountertermEvaluation.entryProgram line 65
  14. opaque OAI.ContinuumCoulomb.CountertermEvaluation.offsiteProgram line 69
  15. opaque OAI.ContinuumCoulomb.CountertermEvaluation.offsiteEnvironmentProgram line 79
  16. opaque OAI.ContinuumCoulomb.CountertermEvaluation.rowProgram line 90
  17. def OAI.ContinuumCoulomb.CountertermEvaluation.certificate line 106