OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceThresholdGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual rational output gap is at least one at a fixed polynomial amplification. The same scale also dominates the numerical error budget.

  1. theorem OAI.ContinuumCoulomb.exists_source_gap_offset line 13
  2. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.gap_ge_one line 40