OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourTensorCoefficientBounds.lean
10 declarations, 0 contain sorry, 0 declared as axioms
Polynomial bounds for the internal counterterm coefficients.
- theorem
OAI.ContinuumCoulomb.qmaFourCouplingFactor_nonnegline 12 - theorem
OAI.ContinuumCoulomb.qmaFourCouplingFactor_boundline 16 - theorem
OAI.ContinuumCoulomb.qmaFourAxisShift_abs_boundline 28 - theorem
OAI.ContinuumCoulomb.qmaFourAxisScale_abs_boundline 31 - theorem
OAI.ContinuumCoulomb.qmaFourAxisSign_absline 35 - theorem
OAI.ContinuumCoulomb.qmaFourCounterA_boundline 38 - theorem
OAI.ContinuumCoulomb.qmaFourCounterB_boundline 47 - theorem
OAI.ContinuumCoulomb.qmaFourTensorCounterterm_linear_boundline 59 - theorem
OAI.ContinuumCoulomb.qmaFourTensorFamilyCounterterm_boundline 66 - theorem
OAI.ContinuumCoulomb.qmaFourTensorFamilyCounterterm_starline 73