OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabPlanarIntegral.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact horizontal-plane Coulomb differences. The individually divergent plane integrals are never separated; their integrable difference has a finite antiderivative and a zero limit at infinity.

  1. def OAI.ContinuumCoulomb.slabRootDifference line 17
  2. def OAI.ContinuumCoulomb.slabRadialDifference line 20
  3. theorem OAI.ContinuumCoulomb.slabRootDifference_quotient line 23
  4. theorem OAI.ContinuumCoulomb.slabRootDifference_tendsto line 32
  5. theorem OAI.ContinuumCoulomb.slabRootDifference_hasDerivAt line 40
  6. theorem OAI.ContinuumCoulomb.slabRadialDifference_nonnegative line 53
  7. theorem OAI.ContinuumCoulomb.slabRadialDifference_integrable line 61
  8. theorem OAI.ContinuumCoulomb.slabRadialDifference_integral line 78
  9. theorem OAI.ContinuumCoulomb.slabPlanarDifference_integrable line 85
  10. theorem OAI.ContinuumCoulomb.slabPlanarDifference_integral line 94

    Source documentation

    Exact difference of two horizontal Coulomb plane integrals.

    theorem slabPlanarDifference_integral {A B : ℝ} (hA : 0 < A) (hB : 0 < B) :
    (∫ p : PlanarPosition, coulombLineKernel A ‖p‖-coulombLineKernel B ‖p‖) =
      2*Real.pi*(Real.sqrt B-Real.sqrt A) := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.coulombLineKernel