OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingCoefficientBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coefficient envelopes for the actual rational crossing layer. The bounds include its scalar counterterms.

  1. theorem OAI.ContinuumCoulomb.qmaCrossingWeight_abs_le line 13
  2. theorem OAI.ContinuumCoulomb.qmaCrossingAmplitude_abs_le line 21
  3. theorem OAI.ContinuumCoulomb.qmaCrossingOffset_abs_le line 30
  4. def OAI.ContinuumCoulomb.qmaCrossingBudget line 40
  5. def OAI.ContinuumCoulomb.qmaCrossingRadiusBound line 43
  6. def OAI.ContinuumCoulomb.qmaCrossingCoefficientBound line 46
  7. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.scale_abs_bound line 52
  8. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.output_weight_abs_le line 91
  9. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.output_constant_abs_le line 110
  10. theorem OAI.ContinuumCoulomb.QMARationalCrossingLayer.output_coefficientBound line 133