OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedCoulombTranslation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Direct Coulomb coefficients as actual translated-density profiles.

  1. def OAI.ContinuumCoulomb.planarCenter line 11
  2. theorem OAI.ContinuumCoulomb.planarCenter_norm line 13
  3. theorem OAI.ContinuumCoulomb.planarCenter_sub line 19
  4. theorem OAI.ContinuumCoulomb.planarCenter_norm_sub line 25
  5. theorem OAI.ContinuumCoulomb.continuumLocalizedMode_translate line 28
  6. theorem OAI.ContinuumCoulomb.localizedDensity_translate line 33
  7. theorem OAI.ContinuumCoulomb.localizedDensity_potential_translate line 37
  8. def OAI.ContinuumCoulomb.localizedCoulombProfileAt line 50
  9. theorem OAI.ContinuumCoulomb.localizedCoulombProfileAt_eq line 54
  10. def OAI.ContinuumCoulomb.localizedCoulombProfile line 62