OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitSubdivisionNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The subdivision counterterm is scalar, Hermitian and polynomially bounded.

  1. theorem OAI.ContinuumCoulomb.qmaSubdivisionCounter_real line 14
  2. theorem OAI.ContinuumCoulomb.qmaSubdivisionCounter_star line 23
  3. theorem OAI.ContinuumCoulomb.qmaSubdivisionLow_star line 29
  4. theorem OAI.ContinuumCoulomb.qmaSubdivisionCounter_norm line 34
  5. theorem OAI.ContinuumCoulomb.qmaSubdivisionLow_norm line 45
  6. theorem OAI.ContinuumCoulomb.qmaSubdivisionTarget_norm line 55
  7. theorem OAI.ContinuumCoulomb.qmaScalarCoupling_sum line 65
  8. theorem OAI.ContinuumCoulomb.qmaSpinMatrix_zero line 69
  9. theorem OAI.ContinuumCoulomb.qmaThirdWeight_neg line 73