OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/HoppingQuadrature.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Literal compact contact quadrature, using the already certified resolvent program at each translated rational point.

  1. abbrev OAI.ContinuumCoulomb.HoppingQuadrature.Settings line 13
  2. abbrev OAI.ContinuumCoulomb.HoppingQuadrature.Input line 14
  3. def OAI.ContinuumCoulomb.HoppingQuadrature.settingsCode line 16
  4. def OAI.ContinuumCoulomb.HoppingQuadrature.sample line 19
  5. def OAI.ContinuumCoulomb.HoppingQuadrature.value line 23
  6. opaque OAI.ContinuumCoulomb.HoppingQuadrature.sampleProgram line 25
  7. opaque OAI.ContinuumCoulomb.HoppingQuadrature.program line 39
  8. def OAI.ContinuumCoulomb.HoppingQuadrature.certificate line 43
  9. theorem OAI.ContinuumCoulomb.HoppingQuadrature.sample_error line 47
  10. theorem OAI.ContinuumCoulomb.HoppingQuadrature.error line 60