OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedRawDensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Unnormalized packets used by the literal Coulomb quadrature. Squaring the normalization cancels the Gaussian square root, so the final quotient uses only the already certified planar mass, frequency and pi evaluators.

  1. def OAI.ContinuumCoulomb.localizedRawDensity line 13
  2. def OAI.ContinuumCoulomb.localizedRawMass line 17
  3. theorem OAI.ContinuumCoulomb.localizedRawMass_positive line 20
  4. theorem OAI.ContinuumCoulomb.localizedRawDensity_nonnegative line 25
  5. theorem OAI.ContinuumCoulomb.localizedRawDensity_le_one line 29
  6. theorem OAI.ContinuumCoulomb.localizedRawDensity_eq_normalized line 37
  7. theorem OAI.ContinuumCoulomb.localizedRawDensity_integrable line 46
  8. theorem OAI.ContinuumCoulomb.localizedRawDensity_mass line 52
  9. theorem OAI.ContinuumCoulomb.localizedRawMass_square line 57
  10. def OAI.ContinuumCoulomb.localizedRawCoulombBox line 62
  11. theorem OAI.ContinuumCoulomb.localizedRawCoulombBox_eq line 66
  12. theorem OAI.ContinuumCoulomb.localizedRawCoulombBox_quotient line 77