OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/OneBodyScaleBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The amplified matrix error decays after retaining the smallness of the shifted matrix in the change of basis.

  1. theorem OAI.ContinuumCoulomb.logarithmic_separation_overlap line 11
  2. theorem OAI.ContinuumCoulomb.matrix_monomial_bound line 27
  3. theorem OAI.ContinuumCoulomb.one_body_scale_identity line 37
  4. theorem OAI.ContinuumCoulomb.one_body_scale_bound line 51