OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceFiniteBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-Hamiltonian bounds used before selecting the source geometry and numerical precision.

  1. theorem OAI.ContinuumCoulomb.exists_target_hopping_exponent line 13
  2. theorem OAI.ContinuumCoulomb.localLeakageBound_antitone line 40
  3. theorem OAI.ContinuumCoulomb.exists_source_leakage_threshold line 48