OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedOneBodyMatrix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual spinful one-body matrix is precisely the corrected spatial matrix, repeated in the two conserved spin components.

  1. theorem OAI.ContinuumCoulomb.localizedSpinResidual_matrix line 16
  2. theorem OAI.ContinuumCoulomb.localizedSpin_nuclear_integrable line 37
  3. theorem OAI.ContinuumCoulomb.localizedSpin_nuclear_matrix line 46
  4. theorem OAI.ContinuumCoulomb.localizedSpin_oneBody_matrix line 57