OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedDensityMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite second moment of the actual localized probability density. It supplies a polynomial finite-box truncation radius, uniformly in the relative displacement appearing in a direct Coulomb coefficient.

  1. theorem OAI.ContinuumCoulomb.quadratic_exponential_bound line 14
  2. theorem OAI.ContinuumCoulomb.planarResolventMode_second_moment_integrable line 28
  3. theorem OAI.ContinuumCoulomb.normalizedPlanarMode_second_moment_integrable line 55
  4. theorem OAI.ContinuumCoulomb.localizedDensity_second_moment_integrable line 60
  5. def OAI.ContinuumCoulomb.localizedDensitySecondMoment line 78
  6. theorem OAI.ContinuumCoulomb.localizedDensitySecondMoment_nonnegative line 81
  7. theorem OAI.ContinuumCoulomb.localizedDensity_tail_of_norm line 85