OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CappedCoulombKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A bounded Lipschitz kernel for literal Coulomb quadrature. The original singular potential differs only inside the cap radius; the next theorem controls that error by the actual Coulomb mass of the small ball.

  1. def OAI.ContinuumCoulomb.cappedCoulombKernel line 13
  2. theorem OAI.ContinuumCoulomb.cappedCoulombKernel_nonnegative line 15
  3. theorem OAI.ContinuumCoulomb.cappedCoulombKernel_le line 20
  4. theorem OAI.ContinuumCoulomb.cappedCoulombKernel_continuous line 24
  5. theorem OAI.ContinuumCoulomb.cappedCoulombKernel_norm_sub line 30
  6. theorem OAI.ContinuumCoulomb.cappedCoulombKernel_difference line 52
  7. def OAI.ContinuumCoulomb.cappedCoulombPotential line 69
  8. theorem OAI.ContinuumCoulomb.cappedCoulombPotential_integrable line 72
  9. theorem OAI.ContinuumCoulomb.cappedCoulombPotential_nonnegative line 82
  10. theorem OAI.ContinuumCoulomb.cappedCoulombPotential_le line 87
  11. theorem OAI.ContinuumCoulomb.cappedCoulombPotential_norm_sub line 95
  12. theorem OAI.ContinuumCoulomb.cappedCoulombPotential_continuous line 115
  13. theorem OAI.ContinuumCoulomb.cappedCoulombPotential_error line 123