OAI/MathematicalPhysics/ContinuumCoulomb/Programs/PolynomialHoppingSmallness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit natural exponents make calibrated hopping perturbatively small and leave an inverse-polynomial fraction of its squared scale.

  1. theorem OAI.ContinuumCoulomb.pow_mul_inverse_add line 13
  2. theorem OAI.ContinuumCoulomb.inverse_power_lt_half line 18
  3. theorem OAI.ContinuumCoulomb.polynomial_hopping_smallness line 27
  4. theorem OAI.ContinuumCoulomb.polynomial_hubbard_error_budget line 70