OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/TransportedGrid.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The far-cell inverse-fifth sum after the actual density transport. Its constant does not depend on the slab's horizontal extent.

  1. theorem OAI.ContinuumCoulomb.transported_far_cube_distances line 14
  2. theorem OAI.ContinuumCoulomb.transported_inverseFifth_far_cube_bound line 29
  3. theorem OAI.ContinuumCoulomb.moser_inverseFifth_grid_sum_bound line 60