OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedCoulombBox.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual direct coefficient is approximated by a bounded integral on a six-dimensional rational cube. The cap and truncation errors are uniform in the relative displacement of the two fixed density packets.

  1. def OAI.ContinuumCoulomb.coulombNumericalBox line 15
  2. theorem OAI.ContinuumCoulomb.coulombNumericalBox_measurable line 18
  3. theorem OAI.ContinuumCoulomb.coulombNumericalBox_outside line 23
  4. def OAI.ContinuumCoulomb.localizedCappedProfile line 30
  5. theorem OAI.ContinuumCoulomb.localizedCappedProfile_eq line 34
  6. def OAI.ContinuumCoulomb.localizedCoulombBoxIntegral line 58
  7. theorem OAI.ContinuumCoulomb.localizedCappedProfile_box_error line 63
  8. theorem OAI.ContinuumCoulomb.localizedCoulombProfile_box_error line 81