OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedCoulomb.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Finite actual Coulomb interactions of the localized densities. Bounded probability densities permit the existing elementary near/far Coulomb bound; no interaction coefficient is introduced as a spectral input.

  1. def OAI.ContinuumCoulomb.localizedAmplitudeBound line 14
  2. theorem OAI.ContinuumCoulomb.localizedAmplitudeBound_positive line 18
  3. theorem OAI.ContinuumCoulomb.continuumLocalizedMode_le line 23
  4. def OAI.ContinuumCoulomb.localizedDensity line 35
  5. theorem OAI.ContinuumCoulomb.localizedDensity_continuous line 38
  6. theorem OAI.ContinuumCoulomb.localizedDensity_nonnegative line 41
  7. theorem OAI.ContinuumCoulomb.localizedDensity_positive line 44
  8. theorem OAI.ContinuumCoulomb.localizedDensity_integrable line 48
  9. theorem OAI.ContinuumCoulomb.localizedDensity_mass line 53
  10. theorem OAI.ContinuumCoulomb.localizedDensity_bound line 56
  11. def OAI.ContinuumCoulomb.localizedPotentialBound line 62
  12. theorem OAI.ContinuumCoulomb.localizedDensity_coulomb_integrable_bound line 65
  13. theorem OAI.ContinuumCoulomb.localizedDensity_potential_nonnegative line 76
  14. theorem OAI.ContinuumCoulomb.localizedDensity_potential_continuous line 81
  15. def OAI.ContinuumCoulomb.localizedCoulombCoeff line 86
  16. theorem OAI.ContinuumCoulomb.localizedCoulombCoeff_integrable line 89
  17. theorem OAI.ContinuumCoulomb.localizedCoulombCoeff_nonnegative line 99
  18. theorem OAI.ContinuumCoulomb.localizedCoulombCoeff_le line 104