OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedCoulombMatrix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual corrected spatial-spin Coulomb tensor differs from its occupation-diagonal density interaction by the Gram and off-site errors.

  1. theorem OAI.ContinuumCoulomb.correctedLocalizedFourIndex_error line 16
  2. theorem OAI.ContinuumCoulomb.localizedSpinMode_coulomb_integrable line 47
  3. theorem OAI.ContinuumCoulomb.localizedSpinMode_coulomb_tensor line 64
  4. def OAI.ContinuumCoulomb.localizedDensityTensor line 100
  5. theorem OAI.ContinuumCoulomb.localizedSpinMode_coulomb_error line 106