OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitMediatorNorm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Spectator-independent norm estimates for the physical mediator terms.

  1. theorem OAI.ContinuumCoulomb.qmaPauliWord_operator_norm line 17
  2. theorem OAI.ContinuumCoulomb.qmaBitFlipMatrix_square line 21
  3. theorem OAI.ContinuumCoulomb.qmaBitFlipMatrix_star line 25
  4. theorem OAI.ContinuumCoulomb.qmaKronecker_unitary_norm line 31
  5. theorem OAI.ContinuumCoulomb.qmaPauliFlip_operator_norm line 37
  6. theorem OAI.ContinuumCoulomb.qmaOccupation_mulVec line 43
  7. theorem OAI.ContinuumCoulomb.qmaKronecker_occupation_norm line 53
  8. theorem OAI.ContinuumCoulomb.qmaPauliOccupation_operator_norm line 85