OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/TransportedNearForm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual transported Gauss nuclei satisfy the separation hypothesis in the full weak-H1 near-field bound, uniformly over the chosen finite grid.

  1. theorem OAI.ContinuumCoulomb.transportedGauss_separation line 14
  2. theorem OAI.ContinuumCoulomb.transportedGauss_near_form line 25