OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CompactOrbitalDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact cutoff densities for compressed nuclear matrix elements. The fourth-order source bounds grow only cubically in the cutoff radius.

  1. def OAI.ContinuumCoulomb.compactOrbitalDensity line 13
  2. theorem OAI.ContinuumCoulomb.compactOrbitalDensity_nonnegative line 16
  3. theorem OAI.ContinuumCoulomb.compactOrbitalDensity_C4 line 23
  4. theorem OAI.ContinuumCoulomb.compactOrbitalDensity_support line 29
  5. theorem OAI.ContinuumCoulomb.compactOrbitalDensity_hasCompactSupport line 33
  6. theorem OAI.ContinuumCoulomb.ball_supported_jet_integral line 37
  7. theorem OAI.ContinuumCoulomb.compactOrbitalDensity_jets_bounded line 62