OAI/MathematicalPhysics/ContinuumCoulomb/Programs/RationalQuadratureProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Literal tabulation and summation of rational quadrature samples. The sample count is unary; bounds, spacing and evaluator data are encoded as ordinary inputs to the machine.

  1. abbrev OAI.ContinuumCoulomb.RationalQuadratureProgram.Environment line 17
  2. abbrev OAI.ContinuumCoulomb.RationalQuadratureProgram.Input line 18
  3. def OAI.ContinuumCoulomb.RationalQuadratureProgram.environmentCode line 20
  4. def OAI.ContinuumCoulomb.RationalQuadratureProgram.inputCode line 23
  5. def OAI.ContinuumCoulomb.RationalQuadratureProgram.node line 26
  6. def OAI.ContinuumCoulomb.RationalQuadratureProgram.sample line 28
  7. def OAI.ContinuumCoulomb.RationalQuadratureProgram.value line 31
  8. theorem OAI.ContinuumCoulomb.RationalQuadratureProgram.range_sum line 34
  9. def OAI.ContinuumCoulomb.RationalQuadratureProgram.sampleProgram line 40
  10. def OAI.ContinuumCoulomb.RationalQuadratureProgram.program line 53
  11. def OAI.ContinuumCoulomb.RationalQuadratureProgram.certificate line 67
  12. theorem OAI.ContinuumCoulomb.RationalQuadratureProgram.node_cast line 72
  13. theorem OAI.ContinuumCoulomb.RationalQuadratureProgram.value_cast line 76
  14. theorem OAI.ContinuumCoulomb.RationalQuadratureProgram.error line 81