OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedCorrectedOneBody.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual one-body operator including well-depth counterterms. Its shifted matrix is exactly the base multiwell matrix plus the weighted well matrix divided by the physical scale.

  1. def OAI.ContinuumCoulomb.correctedMultiwellAction line 15
  2. def OAI.ContinuumCoulomb.localizedCorrectedOneBodyIntegrand line 20
  3. theorem OAI.ContinuumCoulomb.localizedCorrectedOneBodyIntegrand_eq line 26
  4. theorem OAI.ContinuumCoulomb.localizedCorrectedOneBodyIntegrand_integrable line 47
  5. def OAI.ContinuumCoulomb.localizedCorrectedOneBodyMatrix line 57
  6. theorem OAI.ContinuumCoulomb.localizedCorrectedOneBodyMatrix_eq line 60
  7. theorem OAI.ContinuumCoulomb.localizedCorrectedOneBodyMatrix_scaled line 75