OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CappedWells.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The explicit cap in the isolated-well construction

The quintic transition is the normalized integral of a positive multiple of s²(1-s)². Capping removes a whole neighbourhood of both nuclear poles. The resulting pointwise bound is uniform in the secondary displacements, as required before any energy tuning is carried out.

  1. def OAI.ContinuumCoulomb.wellTransition line 18
  2. theorem OAI.ContinuumCoulomb.wellTransition_bounds line 20
  3. def OAI.ContinuumCoulomb.wellCap line 33
  4. theorem OAI.ContinuumCoulomb.wellCap_eq_zero line 36
  5. theorem OAI.ContinuumCoulomb.wellCap_eq_one line 39
  6. theorem OAI.ContinuumCoulomb.wellCap_bounds line 43
  7. theorem OAI.ContinuumCoulomb.wellCap_nonzero_radius line 50
  8. def OAI.ContinuumCoulomb.sitePotential line 56
  9. def OAI.ContinuumCoulomb.cappedSitePotential line 60
  10. theorem OAI.ContinuumCoulomb.sitePotential_nonneg line 63
  11. theorem OAI.ContinuumCoulomb.cappedSitePotential_nonneg line 68
  12. theorem OAI.ContinuumCoulomb.cappedSitePotential_zero_near_primary line 73
  13. theorem OAI.ContinuumCoulomb.cappedSitePotential_zero_near_secondary line 81

    Source documentation

    The cap removes the secondary pole together with an explicit surrounding ball; the cancellation is not merely a convention for the value at the pole.

    theorem cappedSitePotential_zero_near_secondary {D q q' : ℝ}
    (hD : 128 ≤ D) (center displacement x : Position)
    (hdisp : ‖displacement‖ ≤ 4)
    (hx : ‖x - center - displacement‖ ≤ D / 32) :
    cappedSitePotential D q q' center displacement x = 0 := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.cappedSitePotential

  14. theorem OAI.ContinuumCoulomb.cappedSitePotential_bound line 95
  15. def OAI.ContinuumCoulomb.backgroundPotential line 128
  16. theorem OAI.ContinuumCoulomb.backgroundPotential_bounds line 132