OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteOneBodyCorrection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual corrected one-body matrix entries, including the singular nuclear error. Finite change of basis preserves the quantitative entrywise estimates.

  1. theorem OAI.ContinuumCoulomb.finiteTwoIndexChange_error line 17
  2. theorem OAI.ContinuumCoulomb.integral_finite_bilinear line 36
  3. def OAI.ContinuumCoulomb.correctedManufacturedOneBodyMatrix line 58
  4. theorem OAI.ContinuumCoulomb.correctedManufacturedOneBodyMatrix_eq line 62
  5. theorem OAI.ContinuumCoulomb.correctedManufacturedOneBodyMatrix_error line 74
  6. def OAI.ContinuumCoulomb.correctedNuclearOneBodyMatrix line 100
  7. theorem OAI.ContinuumCoulomb.correctedNuclearOneBodyMatrix_error line 105