OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitMediatorPhysical.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The physical parallel-qubit Hamiltonian has the calculated vacuum column.

  1. theorem OAI.ContinuumCoulomb.qmaSliceColumn_right_mul line 15
  2. def OAI.ContinuumCoulomb.qmaPhysicalPenaltyMatrix line 20
  3. def OAI.ContinuumCoulomb.qmaPhysicalMediatorMatrix line 23
  4. theorem OAI.ContinuumCoulomb.qmaPhysicalPenalty_vacuum line 27
  5. theorem OAI.ContinuumCoulomb.qmaLiftedLow_vacuum line 33
  6. theorem OAI.ContinuumCoulomb.qmaPhysicalMediator_vacuum line 41
  7. theorem OAI.ContinuumCoulomb.qmaAncillaDiagonal_real_star line 54
  8. theorem OAI.ContinuumCoulomb.qmaAncillaOccupation_star line 65
  9. theorem OAI.ContinuumCoulomb.qmaMediatorPerturbation_star line 74
  10. theorem OAI.ContinuumCoulomb.qmaPhysicalMediator_star line 83