OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/WellFieldOrbitalResidual.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The cutoff and depth-counterterm contribution to the actual localized one-particle residual. The estimate uses polynomially many spatial modes.

  1. theorem OAI.ContinuumCoulomb.planarWellSum_abs_bound line 14
  2. theorem OAI.ContinuumCoulomb.countertermWellSum_sub_eq line 23
  3. theorem OAI.ContinuumCoulomb.countertermWellSum_sub_abs_bound line 33
  4. theorem OAI.ContinuumCoulomb.manufacturedWellField_sub_abs_bound line 52
  5. def OAI.ContinuumCoulomb.wellFieldOrbitalResidual line 77
  6. theorem OAI.ContinuumCoulomb.wellFieldOrbitalResidual_square_integrable line 82
  7. theorem OAI.ContinuumCoulomb.wellFieldOrbitalResidual_square_bound line 101