OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabConfinement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuumCoulomb.slabPlanarBox_compact line 14
2. def OAI.ContinuumCoulomb.slabPlanarSection line 35
3. theorem OAI.ContinuumCoulomb.slabPlanarSection_kernel_integrable line 38
4. theorem OAI.ContinuumCoulomb.slabPlanarSection_intervalIntegrable line 46
5. theorem OAI.ContinuumCoulomb.slabPlanarSection_sub line 56
6. theorem OAI.ContinuumCoulomb.regularizedSlab_vertical_interval line 67
7. def OAI.ContinuumCoulomb.slabPlaneError line 75
8. theorem OAI.ContinuumCoulomb.slabPlaneError_bound line 79
9. theorem OAI.ContinuumCoulomb.regularizedSlab_error_identity line 89
10. theorem OAI.ContinuumCoulomb.regularizedSlab_confinement_error line 109

    Source documentation

    The regularized finite slab differs from its one-dimensional profile by at most the horizontal inverse-cube tail.

    theorem regularizedSlab_confinement_error {epsilon rho H S z : ℝ}
        (hepsilon : epsilon ≠ 0) (hrho : 0 ≤ rho) (hH : 0 < H)
        (hS : 0 ≤ S) (hz : |z| ≤ S) :
        |regularizedSlabPotential epsilon rho H S (slabAxisPoint z)-
          regularizedSlabPotential epsilon rho H S (slabAxisPoint 0)-
          2*Real.pi*rho*slabRegularizedProfile epsilon S z| ≤ 6*Real.pi*rho*S^3/H := by
    …

    Mentions: OAI.ContinuumCoulomb.regularizedSlabPotential, OAI.ContinuumCoulomb.slabAxisPoint, OAI.ContinuumCoulomb.slabRegularizedProfile

11. theorem OAI.ContinuumCoulomb.slabPotential_axis_error line 131

    Source documentation

    The actual singular finite-slab potential has the quadratic profile, with a uniform error controlled by its finite horizontal extent.

    theorem slabPotential_axis_error {rho H S z : ℝ} (hrho : 0 ≤ rho)
        (hH : 0 < H) (hS : 0 ≤ S) (hz : |z| ≤ S) :
        |slabPotential rho H S (slabAxisPoint z)-slabPotential rho H S 0-
          2*Real.pi*rho*z^2| ≤ 6*Real.pi*rho*S^3/H := by
    …

    Mentions: OAI.ContinuumCoulomb.slabPotential, OAI.ContinuumCoulomb.slabAxisPoint

12. theorem OAI.ContinuumCoulomb.slabPotential_confinement line 157

    Source documentation

    Global capped-quadratic confinement in the physical vertical coordinate.

    theorem slabPotential_confinement {rho H S : ℝ} (hrho : 0 ≤ rho)
        (hH : 0 < H) (hS : 0 ≤ S) (y : Position) :
        2*Real.pi*rho*min ((y 2)^2) (S^2)-6*Real.pi*rho*S^3/H ≤
          slabPotential rho H S y-slabPotential rho H S 0 := by
    …

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.slabPotential