OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalSixQuadrature.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Six-coordinate rational cubature, as three literal rectangle programs. The same finite mesh is retained in each register environment.

  1. abbrev OAI.ContinuumCoulomb.RationalSixQuadrature.Pair line 12
  2. abbrev OAI.ContinuumCoulomb.RationalSixQuadrature.Input line 13
  3. abbrev OAI.ContinuumCoulomb.RationalSixQuadrature.Evaluator line 14
  4. def OAI.ContinuumCoulomb.RationalSixQuadrature.pairCode line 16
  5. def OAI.ContinuumCoulomb.RationalSixQuadrature.augment line 18
  6. def OAI.ContinuumCoulomb.RationalSixQuadrature.remember line 21
  7. def OAI.ContinuumCoulomb.RationalSixQuadrature.inner line 23
  8. def OAI.ContinuumCoulomb.RationalSixQuadrature.middle line 26
  9. def OAI.ContinuumCoulomb.RationalSixQuadrature.outer line 29
  10. def OAI.ContinuumCoulomb.RationalSixQuadrature.value line 32
  11. opaque OAI.ContinuumCoulomb.RationalSixQuadrature.augmentProgram line 35
  12. opaque OAI.ContinuumCoulomb.RationalSixQuadrature.rememberProgram line 49
  13. opaque OAI.ContinuumCoulomb.RationalSixQuadrature.middleProgram line 58
  14. opaque OAI.ContinuumCoulomb.RationalSixQuadrature.outerProgram line 66
  15. opaque OAI.ContinuumCoulomb.RationalSixQuadrature.program line 76
  16. def OAI.ContinuumCoulomb.RationalSixQuadrature.certificate line 83
  17. theorem OAI.ContinuumCoulomb.RationalSixQuadrature.value_cast line 90