OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/TransportedNearGrid.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Near cells have uniformly bounded continuous Coulomb mass after the actual Moser transport. The bound is independent of the enclosing box.

  1. theorem OAI.ContinuumCoulomb.transported_near_cube_distance line 15
  2. theorem OAI.ContinuumCoulomb.transported_near_kernel_eq line 27
  3. theorem OAI.ContinuumCoulomb.moser_near_grid_integral_bound line 36