OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPathPolynomialBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial coefficient envelopes for the actual selected path subdivision, uniform in the selected set and its parity choices.

  1. def OAI.ContinuumCoulomb.qmaPathBudget line 13
  2. def OAI.ContinuumCoulomb.qmaPathRadiusBound line 16
  3. def OAI.ContinuumCoulomb.qmaPathCoefficientBound line 19
  4. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.CoefficientBound line 25
  5. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.pathScale_abs_bound line 28
  6. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.subdivide_coefficientBound line 72