OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombTargetLipschitz.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A quantitative modulus for the actual calibrated hopping residual. The Coulomb gap keeps the square root away from zero, so ordinary dyadic bisection needs no lower derivative bound.

  1. theorem OAI.ContinuumCoulomb.sqrt_abs_sub_le_of_lower line 12
  2. theorem OAI.ContinuumCoulomb.localizedCoulombProfile_abs_sub line 28
  3. def OAI.ContinuumCoulomb.coulombTargetLipschitzConstant line 35
  4. theorem OAI.ContinuumCoulomb.coulombTargetLipschitzConstant_nonnegative line 38
  5. theorem OAI.ContinuumCoulomb.coulombHoppingTarget_abs_sub line 46
  6. theorem OAI.ContinuumCoulomb.calibratedResidual_abs_sub line 73