OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitMediatorPenalty.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

An invertible diagonal extension of the physical excitation penalty. The extension agrees with the physical penalty on the actual complement.

  1. def OAI.ContinuumCoulomb.qmaPaddedExcitationNumber line 14
  2. theorem OAI.ContinuumCoulomb.qmaPaddedExcitationNumber_pos line 18
  3. theorem OAI.ContinuumCoulomb.qmaPaddedExcitationNumber_single line 24
  4. def OAI.ContinuumCoulomb.qmaPaddedWeight line 28
  5. def OAI.ContinuumCoulomb.qmaPaddedPenalty line 31
  6. def OAI.ContinuumCoulomb.qmaPaddedInverse line 34
  7. theorem OAI.ContinuumCoulomb.qmaPaddedPenalty_gap line 38
  8. theorem OAI.ContinuumCoulomb.qmaPaddedPenalty_inverse line 47
  9. theorem OAI.ContinuumCoulomb.qmaPaddedInverse_norm line 55
  10. theorem OAI.ContinuumCoulomb.qmaAncillaDiagonal_real_operator line 63
  11. theorem OAI.ContinuumCoulomb.qmaPaddedInverse_column line 71