OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalTripleQuadrature.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Three-coordinate rational cubature, using the already proved literal one- and two-coordinate summation programs.

  1. abbrev OAI.ContinuumCoulomb.RationalTripleQuadrature.Input line 13
  2. abbrev OAI.ContinuumCoulomb.RationalTripleQuadrature.Evaluator line 14
  3. def OAI.ContinuumCoulomb.RationalTripleQuadrature.augment line 16
  4. def OAI.ContinuumCoulomb.RationalTripleQuadrature.remember line 19
  5. def OAI.ContinuumCoulomb.RationalTripleQuadrature.inner line 21
  6. def OAI.ContinuumCoulomb.RationalTripleQuadrature.outer line 23
  7. def OAI.ContinuumCoulomb.RationalTripleQuadrature.value line 26
  8. opaque OAI.ContinuumCoulomb.RationalTripleQuadrature.augmentProgram line 29
  9. opaque OAI.ContinuumCoulomb.RationalTripleQuadrature.rememberProgram line 41
  10. opaque OAI.ContinuumCoulomb.RationalTripleQuadrature.outerProgram line 49
  11. opaque OAI.ContinuumCoulomb.RationalTripleQuadrature.program line 56
  12. def OAI.ContinuumCoulomb.RationalTripleQuadrature.certificate line 63
  13. theorem OAI.ContinuumCoulomb.RationalTripleQuadrature.value_cast line 69