OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabLineIntegral.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Centered-interval comparison for the actual one-coordinate Coulomb integrals. It is the coordinatewise monotonicity step in the slab estimate.

  1. def OAI.ContinuumCoulomb.centeredLineIntegral line 14
  2. theorem OAI.ContinuumCoulomb.centeredLineIntegral_translate line 17
  3. theorem OAI.ContinuumCoulomb.centeredLineIntegral_hasDerivAt line 22
  4. theorem OAI.ContinuumCoulomb.centeredLineIntegral_even line 37
  5. theorem OAI.ContinuumCoulomb.centeredLineIntegral_antitone line 46
  6. theorem OAI.ContinuumCoulomb.centeredLineIntegral_le_center line 62
  7. def OAI.ContinuumCoulomb.coulombLineKernel line 79

    Source documentation

    A nonsingular Coulomb line section, with the other two squared coordinates (and optional regularization) collected in A.

    def coulombLineKernel (A t : ℝ) : ℝ := (Real.sqrt (A+t^2))⁻¹
  8. theorem OAI.ContinuumCoulomb.coulombLineKernel_continuous line 81
  9. theorem OAI.ContinuumCoulomb.coulombLineKernel_radial_antitone line 88
  10. theorem OAI.ContinuumCoulomb.coulombLineIntegral_antitone line 95
  11. theorem OAI.ContinuumCoulomb.coulombLineIntegral_le_center line 100