OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryMatrix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual finite Hermitian circuit-history Hamiltonian.

  1. abbrev OAI.ContinuumCoulomb.QMAPropagationBasis line 13
  2. def OAI.ContinuumCoulomb.qmaPropagationMap line 16
  3. def OAI.ContinuumCoulomb.qmaPropagationMatrix line 38
  4. def OAI.ContinuumCoulomb.qmaInitialDiagonal line 42
  5. def OAI.ContinuumCoulomb.qmaFinalDiagonal line 45
  6. def OAI.ContinuumCoulomb.qmaHistoryHamiltonian line 48
  7. theorem OAI.ContinuumCoulomb.qmaHistoryHamiltonian_hermitian line 53