OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourcePositiveMargin.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal positive-spin thresholds retain a quantitative part of the rounding budget. This margin pays for the later Hubbard and continuum errors.

  1. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.normalization_margin line 11
  2. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.source_positive_margin line 25
  3. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.source_positive_yes_margin line 34
  4. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.source_positive_no_margin line 46
  5. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.output_yes_margin line 63
  6. theorem OAI.ContinuumCoulomb.SourcePositiveProgram.output_no_margin line 72