OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/GridNuclei.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The transported Gauss cloud is an actual collection of distinct unit nuclei. Its physical form has exactly the slab-origin energy offset.

  1. theorem OAI.ContinuumCoulomb.gaussLatticePoint_injective line 15
  2. def OAI.ContinuumCoulomb.gridNuclei line 23
  3. theorem OAI.ContinuumCoulomb.gridNuclei_attraction line 34
  4. theorem OAI.ContinuumCoulomb.gridNuclearPotential_attraction line 45
  5. theorem OAI.ContinuumCoulomb.manufactured_grid_split line 54