OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteWellResidual.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite vertical cutoff error after retaining the intended well-depth counterterms. Its bound decays with the slab height and does not include the counterterm itself as an error.

  1. theorem OAI.ContinuumCoulomb.countertermWellSum_abs_bound line 14
  2. def OAI.ContinuumCoulomb.finiteWellOrbitalResidual line 25
  3. theorem OAI.ContinuumCoulomb.finiteWellOrbitalResidual_continuous line 30
  4. theorem OAI.ContinuumCoulomb.finiteWellOrbitalResidual_square_bound line 37