OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CompactSourcePairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fubini identities for nonnegative compact source densities and the actual transported nuclear potential. No separation from a nuclear pole is required for these identities.

  1. theorem OAI.ContinuumCoulomb.compact_source_transport_integrable line 14
  2. theorem OAI.ContinuumCoulomb.compact_source_transport_pairing line 37
  3. theorem OAI.ContinuumCoulomb.gridNuclearPotential_pairing line 49