OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumDistributedMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The distributed-input history is an actual Hermitian matrix on all unary strings.

  1. def OAI.ContinuumCoulomb.qmaUnaryDistributedDiagonal line 13
  2. theorem OAI.ContinuumCoulomb.qmaUnaryDistributedDiagonal_form line 18
  3. def OAI.ContinuumCoulomb.qmaUnaryDistributedHamiltonian line 28
  4. theorem OAI.ContinuumCoulomb.qmaUnaryDistributedHamiltonian_hermitian line 36
  5. theorem OAI.ContinuumCoulomb.qmaUnaryDistributedHamiltonian_form line 47
  6. def OAI.ContinuumCoulomb.qmaDistributedInputSites line 61
  7. def OAI.ContinuumCoulomb.qmaDistributedInputTerm line 66
  8. theorem OAI.ContinuumCoulomb.qmaDistributedInputTerm_local line 72
  9. theorem OAI.ContinuumCoulomb.qmaDistributedInputSites_card line 85
  10. theorem OAI.ContinuumCoulomb.qmaUnaryDistributedInput_reindex line 94