OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/SlowLogarithmicExtent.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic spacing contributes only a hundredth of the adjustable exponent. This closes the final analytic parameter inequalities without a circular dependence on the spatial extent.

  1. theorem OAI.ContinuumCoulomb.ContactMediator.hundred_mul_le_two_pow line 12
  2. theorem OAI.ContinuumCoulomb.ContactMediator.exponent_le_slow_power line 22
  3. theorem OAI.ContinuumCoulomb.ContactMediator.slow_logarithmic_extent line 30
  4. theorem OAI.ContinuumCoulomb.ContactMediator.slow_extent_parameter_closure line 49