OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/InverseFifthGrid.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Inverse-fifth far-cell sums are bounded independently of box volume. The proof compares each actual cube to the integrable radial tail.

  1. theorem OAI.ContinuumCoulomb.far_cube_distances line 15
  2. theorem OAI.ContinuumCoulomb.inverseFifth_far_cube_bound line 26
  3. theorem OAI.ContinuumCoulomb.inverseFifth_grid_sum_bound line 48
  4. theorem OAI.ContinuumCoulomb.coulomb_far_grid_error line 65