OAI/MathematicalPhysics/ContinuumCoulomb/Programs/RationalRectangleProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A literal two-coordinate rational quadrature. The same mesh in both coordinates is enough for the normalization and compact contact integrals.

  1. abbrev OAI.ContinuumCoulomb.RationalRectangleProgram.Input line 13
  2. def OAI.ContinuumCoulomb.RationalRectangleProgram.inputCode line 15
  3. def OAI.ContinuumCoulomb.RationalRectangleProgram.lineInput line 18
  4. def OAI.ContinuumCoulomb.RationalRectangleProgram.line line 21
  5. def OAI.ContinuumCoulomb.RationalRectangleProgram.outerInput line 24
  6. def OAI.ContinuumCoulomb.RationalRectangleProgram.value line 27
  7. opaque OAI.ContinuumCoulomb.RationalRectangleProgram.lineInputProgram line 30
  8. opaque OAI.ContinuumCoulomb.RationalRectangleProgram.outerInputProgram line 41
  9. opaque OAI.ContinuumCoulomb.RationalRectangleProgram.program line 48
  10. def OAI.ContinuumCoulomb.RationalRectangleProgram.certificate line 57
  11. theorem OAI.ContinuumCoulomb.RationalRectangleProgram.value_cast line 63