OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarForcing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's explicit planar forcing (1-|r|²)₊¹⁶, including finite smoothness at its support boundary. The positive-part power is represented by a polynomial plus a fractional power of a square, avoiding a nonsmooth positive-part differentiation rule.

  1. def OAI.ContinuumCoulomb.positivePartSixteen line 15
  2. theorem OAI.ContinuumCoulomb.positivePartSixteen_formula line 17
  3. theorem OAI.ContinuumCoulomb.positivePartSixteen_C7 line 30
  4. def OAI.ContinuumCoulomb.planarForcing line 40
  5. theorem OAI.ContinuumCoulomb.planarForcing_C7 line 42
  6. theorem OAI.ContinuumCoulomb.planarForcing_nonnegative line 45
  7. theorem OAI.ContinuumCoulomb.planarForcing_le_one line 48
  8. theorem OAI.ContinuumCoulomb.planarForcing_zero_of_norm_ge_one line 53
  9. theorem OAI.ContinuumCoulomb.planarForcing_support line 59
  10. theorem OAI.ContinuumCoulomb.planarForcing_hasCompactSupport line 66
  11. theorem OAI.ContinuumCoulomb.planarForcing_zero line 70
  12. theorem OAI.ContinuumCoulomb.planarForcing_integrable line 73
  13. theorem OAI.ContinuumCoulomb.planarForcing_integral_positive line 76