OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CorrectedNuclearError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite basis correction of the actual nuclear error form. Only polynomially many orbital matrix entries are summed.

  1. theorem OAI.ContinuumCoulomb.localizedLinearOrbital_weighted_integrable line 13
  2. theorem OAI.ContinuumCoulomb.localizedLinearOrbital_weighted_pairing line 33
  3. theorem OAI.ContinuumCoulomb.correctedLocalizedMode_nuclear_error line 59