OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumDistributedFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A linear-size, five-local term family with distributed initialization checks.

  1. def OAI.ContinuumCoulomb.qmaDistributedQubitHamiltonian line 13
  2. theorem OAI.ContinuumCoulomb.qmaDistributedQubitHamiltonian_decomposition line 18
  3. def OAI.ContinuumCoulomb.qmaDistributedTermSites line 30
  4. def OAI.ContinuumCoulomb.qmaDistributedTermMatrix line 35
  5. theorem OAI.ContinuumCoulomb.qmaDistributedTerm_local line 46
  6. theorem OAI.ContinuumCoulomb.qmaDistributedTerm_support_card line 58
  7. theorem OAI.ContinuumCoulomb.qmaDistributedTerm_hermitian line 70
  8. theorem OAI.ContinuumCoulomb.qmaDistributedTerm_sum line 82