OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitThirdNormBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A rational polynomial budget for the third-order counterterms.

  1. def OAI.ContinuumCoulomb.qmaThirdWeight line 14
  2. theorem OAI.ContinuumCoulomb.qmaThirdWeight_bounds line 16
  3. theorem OAI.ContinuumCoulomb.qmaMatrix_real_smul_norm line 29
  4. theorem OAI.ContinuumCoulomb.qmaMatrix_product_norm line 34
  5. theorem OAI.ContinuumCoulomb.qmaMatrixOperator_neg line 41
  6. theorem OAI.ContinuumCoulomb.qmaThirdPair_norm line 46
  7. theorem OAI.ContinuumCoulomb.qmaThirdCounter_norm line 61