OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedCounterterms.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's actual well-depth counterterms: direct Coulomb sums divided by the fixed positive onsite well integral. Their diagonal action cancels the required linear occupancy term exactly.

  1. def OAI.ContinuumCoulomb.localizedOffsiteSum line 15
  2. def OAI.ContinuumCoulomb.localizedCounterterm line 18
  3. def OAI.ContinuumCoulomb.localizedCountertermBound line 21
  4. theorem OAI.ContinuumCoulomb.localizedOffsiteSum_nonnegative line 23
  5. theorem OAI.ContinuumCoulomb.localizedCounterterm_nonnegative line 31
  6. theorem OAI.ContinuumCoulomb.localizedCountertermBound_nonnegative line 35
  7. theorem OAI.ContinuumCoulomb.localizedOffsiteSum_bound line 38
  8. theorem OAI.ContinuumCoulomb.localizedCounterterm_bound line 50
  9. theorem OAI.ContinuumCoulomb.localizedCounterterm_diagonal line 56
  10. theorem OAI.ContinuumCoulomb.exists_uniform_counterterm_scale line 62