OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUnaryMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual Hermitian matrix on all clock and computation qubits.

  1. abbrev OAI.ContinuumCoulomb.QMAUnaryRow line 12
  2. def OAI.ContinuumCoulomb.qmaUnaryPropagationMap line 14
  3. def OAI.ContinuumCoulomb.qmaUnaryPropagationMatrix line 42
  4. def OAI.ContinuumCoulomb.qmaUnaryClockDiagonal line 45
  5. def OAI.ContinuumCoulomb.qmaUnaryInputDiagonal line 48
  6. def OAI.ContinuumCoulomb.qmaUnaryOutputDiagonal line 51
  7. def OAI.ContinuumCoulomb.qmaUnaryHamiltonian line 54
  8. theorem OAI.ContinuumCoulomb.qmaUnaryPropagationMatrix_form line 60
  9. theorem OAI.ContinuumCoulomb.qmaUnaryHamiltonian_hermitian line 67
  10. theorem OAI.ContinuumCoulomb.qmaUnaryHamiltonian_form line 76