OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalPenalties.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The clock and endpoint penalties are explicit one- and two-qubit terms.

  1. def OAI.ContinuumCoulomb.qmaBitDiagonal line 14
  2. def OAI.ContinuumCoulomb.qmaPairDiagonal line 17
  3. theorem OAI.ContinuumCoulomb.qmaBitDiagonal_local line 21
  4. theorem OAI.ContinuumCoulomb.qmaPairDiagonal_local line 27
  5. def OAI.ContinuumCoulomb.qmaClockFaultTerm line 33
  6. def OAI.ContinuumCoulomb.qmaClockLeftTerm line 38
  7. def OAI.ContinuumCoulomb.qmaClockRightTerm line 42
  8. def OAI.ContinuumCoulomb.qmaInputTerm line 46
  9. def OAI.ContinuumCoulomb.qmaOutputTerm line 51
  10. theorem OAI.ContinuumCoulomb.qmaClockFaultTerm_local line 56
  11. theorem OAI.ContinuumCoulomb.qmaClockLeftTerm_local line 60
  12. theorem OAI.ContinuumCoulomb.qmaClockRightTerm_local line 63
  13. theorem OAI.ContinuumCoulomb.qmaInputTerm_local line 67
  14. theorem OAI.ContinuumCoulomb.qmaOutputTerm_local line 71