OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedCoulombNumerics.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual six-coordinate bounded integrand for Coulomb quadrature, with an explicit error to the original full singular coefficient.

  1. def OAI.ContinuumCoulomb.localizedCappedIntegrand line 13
  2. def OAI.ContinuumCoulomb.localizedCappedCoulombCoeff line 17
  3. theorem OAI.ContinuumCoulomb.localizedCappedIntegrand_integrable line 20
  4. theorem OAI.ContinuumCoulomb.localizedCappedCoulombCoeff_nested line 37
  5. theorem OAI.ContinuumCoulomb.localizedCappedCoulombCoeff_error line 46