OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/WellCapRegularity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

C² regularity of the manuscript's rational quintic nuclear cap.

  1. theorem OAI.ContinuumCoulomb.hasDerivAt_wellSplice line 12
  2. theorem OAI.ContinuumCoulomb.contDiff_two_wellSplice line 45
  3. def OAI.ContinuumCoulomb.wellMiddle line 75
  4. def OAI.ContinuumCoulomb.wellMiddlePrime line 76
  5. def OAI.ContinuumCoulomb.wellMiddleSecond line 77
  6. theorem OAI.ContinuumCoulomb.wellMiddle_hasDerivAt line 80
  7. theorem OAI.ContinuumCoulomb.wellMiddlePrime_hasDerivAt line 87
  8. theorem OAI.ContinuumCoulomb.deriv_wellMiddle line 94
  9. theorem OAI.ContinuumCoulomb.deriv2_wellMiddle line 98
  10. theorem OAI.ContinuumCoulomb.wellCap_contDiff_two line 105

    Source documentation

    All cap data are rational polynomials; both derivatives match the constant pieces at the endpoints of the transition interval.

    theorem wellCap_contDiff_two : ContDiff ℝ 2 wellCap := by
…

    Mentions: OAI.ContinuumCoulomb.wellCap

  11. theorem OAI.ContinuumCoulomb.cappedSitePotential_contDiff_two line 146

    Source documentation

    Despite the two Coulomb poles, the capped field is globally C². The proof uses actual vanishing neighbourhoods at the poles and ordinary differentiation away from them.

    theorem cappedSitePotential_contDiff_two {D q q' : ℝ} (hD : 128 ≤ D)
    (center displacement : Position) (hdisp : ‖displacement‖ ≤ 4) :
    ContDiff ℝ 2 (cappedSitePotential D q q' center displacement) := by
…

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

  12. theorem OAI.ContinuumCoulomb.backgroundPotential_contDiff_two line 182