OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactQuotientBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Stability of the actual contact quotient. A fixed natural guard for the fixed positive normalization integral suffices for all inputs.

  1. theorem OAI.ContinuumCoulomb.planarHoppingNumerator_abs_le_four line 12
  2. def OAI.ContinuumCoulomb.contactNormalizationGuard line 33
  3. theorem OAI.ContinuumCoulomb.contactNormalizationGuard_positive line 36
  4. theorem OAI.ContinuumCoulomb.contactNormalizationGuard_bound line 40
  5. theorem OAI.ContinuumCoulomb.contact_quotient_error line 50