OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarForcingModulus.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An explicit global modulus for the forcing used by the numerical quadrature. Unlike an unspecified compact-support derivative bound, the constant is a fixed integer usable by the literal sample-count program.

  1. theorem OAI.ContinuumCoulomb.clippedSquare_formula line 12
  2. theorem OAI.ContinuumCoulomb.clippedSquare_lipschitz line 21
  3. theorem OAI.ContinuumCoulomb.planarForcing_norm_sub_explicit line 41