OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedGridError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise nuclear replacement on any finite grid: the smooth error is quadratic in the mesh, and the only singular remainder is an explicit sum of near-node kernels, suitable for the proved weak-H1 estimate.

  1. theorem OAI.ContinuumCoulomb.gaussLatticePoint_mem_cube line 15
  2. theorem OAI.ContinuumCoulomb.near_cell_gauss_truncated line 25
  3. theorem OAI.ContinuumCoulomb.manufactured_moser_grid_error line 38