OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteBoxMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite-box correction to the intended one-body matrix. The well-depth counterterm remains part of the target matrix; only its vertical truncation and the finite slab approximation contribute to this error.

  1. def OAI.ContinuumCoulomb.finiteBoxOrbitalResidual line 15
  2. def OAI.ContinuumCoulomb.finiteBoxOrbitalSquaredError line 19
  3. theorem OAI.ContinuumCoulomb.slabOrbitalResidual_continuous line 27
  4. theorem OAI.ContinuumCoulomb.finiteBoxOrbitalResidual_continuous line 34
  5. theorem OAI.ContinuumCoulomb.finiteBoxOrbitalResidual_memLp line 41
  6. theorem OAI.ContinuumCoulomb.finiteBoxOrbitalResidual_square_bound line 54
  7. def OAI.ContinuumCoulomb.manufacturedRawOneBodyMatrix line 77
  8. theorem OAI.ContinuumCoulomb.manufacturedRawOneBodyMatrix_integrand line 81
  9. theorem OAI.ContinuumCoulomb.manufacturedRawOneBodyMatrix_error_integral line 103
  10. theorem OAI.ContinuumCoulomb.manufacturedRawOneBodyMatrix_error line 135