OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedCoulombLipschitz.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A uniform Lipschitz estimate for the actual direct-Coulomb profile.

  1. def OAI.ContinuumCoulomb.localizedCoulombLipschitzConstant line 11
  2. theorem OAI.ContinuumCoulomb.localizedCoulombLipschitzConstant_nonnegative line 15
  3. theorem OAI.ContinuumCoulomb.localizedDensity_potential_norm_sub line 20
  4. theorem OAI.ContinuumCoulomb.localizedCoulombProfileAt_integrable line 29
  5. theorem OAI.ContinuumCoulomb.localizedCoulombProfileAt_norm_sub line 37
  6. theorem OAI.ContinuumCoulomb.localizedCoulombProfileAt_continuous line 65
  7. theorem OAI.ContinuumCoulomb.localizedCoulombProfile_continuous line 72