OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabPlanarTail.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The inverse-cube tail in two horizontal dimensions. Its exact mass is 2π/H, giving the finite-slab truncation error without divergent integrals.

  1. def OAI.ContinuumCoulomb.slabRadialTail line 13
  2. def OAI.ContinuumCoulomb.slabPlanarTail line 16
  3. theorem OAI.ContinuumCoulomb.slabRadialTail_weight line 18
  4. theorem OAI.ContinuumCoulomb.slabRadialTail_weight_integrable line 27
  5. theorem OAI.ContinuumCoulomb.slabRadialTail_weight_integral line 33
  6. theorem OAI.ContinuumCoulomb.slabPlanarTail_integrable line 43
  7. theorem OAI.ContinuumCoulomb.slabPlanarTail_nonnegative line 50
  8. theorem OAI.ContinuumCoulomb.slabPlanarTail_integral line 59

    Source documentation

    The exact horizontal inverse-cube tail mass.

    theorem slabPlanarTail_integral {H : ℝ} (hH : 0 < H) :
    (∫ p, slabPlanarTail H p) = 2*Real.pi/H := by
…

    Mentions: OAI.ContinuumCoulomb.slabPlanarTail

  9. def OAI.ContinuumCoulomb.slabPlanarBox line 72
  10. theorem OAI.ContinuumCoulomb.slabPlanarBox_measurable line 75
  11. theorem OAI.ContinuumCoulomb.slabPlanarBox_compl_norm line 82
  12. theorem OAI.ContinuumCoulomb.slab_regularized_line_difference_uniform line 91
  13. theorem OAI.ContinuumCoulomb.slabPlanarDifference_tail_bound line 112

    Source documentation

    The finite square loses at most the integrable radial tail.

    theorem slabPlanarDifference_tail_bound {H S epsilon z w : ℝ} (hH : 0 < H)
    (hepsilon : epsilon ≠ 0) (hz : |z| ≤ S) (hw : |w| ≤ S) :
    |∫ p in (slabPlanarBox H)ᶜ,
      (coulombLineKernel (epsilon^2+(z-w)^2) ‖p‖-
       coulombLineKernel (epsilon^2+w^2) ‖p‖)| ≤ 3*Real.pi*S^2/H := by
…

    Mentions: OAI.ContinuumCoulomb.slabPlanarBox, OAI.ContinuumCoulomb.coulombLineKernel

  14. theorem OAI.ContinuumCoulomb.slabPlanarDifference_estimate line 155

    Source documentation

    The finite horizontal square differs from the infinite-plane formula by at most the inverse-cube tail.

    theorem slabPlanarDifference_estimate {H S epsilon z w : ℝ} (hH : 0 < H)
    (hepsilon : epsilon ≠ 0) (hz : |z| ≤ S) (hw : |w| ≤ S) :
    |(∫ p in slabPlanarBox H,
       (coulombLineKernel (epsilon^2+(z-w)^2) ‖p‖-
        coulombLineKernel (epsilon^2+w^2) ‖p‖)) -
      2*Real.pi*(Real.sqrt (epsilon^2+w^2)-Real.sqrt (epsilon^2+(z-w)^2))| ≤
        3*Real.pi*S^2/H := by
…

    Mentions: OAI.ContinuumCoulomb.slabPlanarBox, OAI.ContinuumCoulomb.coulombLineKernel