OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitMediatorMatrix.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The literal parallel mediator Hamiltonian and its exact first three vacuum-compressed terms. Single flips have zero third-order compression.

  1. def OAI.ContinuumCoulomb.qmaMediatorFlips line 14
  2. def OAI.ContinuumCoulomb.qmaMediatorOccupations line 18
  3. def OAI.ContinuumCoulomb.qmaMediatorPerturbation line 22
  4. theorem OAI.ContinuumCoulomb.qmaMediatorFlips_vacuum line 26
  5. theorem OAI.ContinuumCoulomb.qmaMediatorOccupations_vacuum line 37
  6. theorem OAI.ContinuumCoulomb.qmaAncillaColumn_identity line 49
  7. theorem OAI.ContinuumCoulomb.qmaMediatorPerturbation_compression line 57
  8. def OAI.ContinuumCoulomb.qmaAncillaDiagonal line 66
  9. theorem OAI.ContinuumCoulomb.qmaAncillaDiagonal_slice line 70
  10. theorem OAI.ContinuumCoulomb.qmaAncillaDiagonal_column line 81
  11. def OAI.ContinuumCoulomb.qmaAncillaInverseWeight line 90
  12. theorem OAI.ContinuumCoulomb.qmaAncillaInverseWeight_single line 93
  13. theorem OAI.ContinuumCoulomb.qmaAncillaInverse_column line 97