OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLocalPauli.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A bounded-support real family expands into only even-Y Pauli words.

  1. abbrev OAI.ContinuumCoulomb.QMALocalPauliTerm line 13
  2. abbrev OAI.ContinuumCoulomb.QMALocalEvenPauliTerm line 16
  3. def OAI.ContinuumCoulomb.qmaLocalPauliWord line 19
  4. def OAI.ContinuumCoulomb.qmaLocalPauliCoefficient line 22
  5. def OAI.ContinuumCoulomb.qmaLocalPauliMatrix line 26
  6. theorem OAI.ContinuumCoulomb.qmaLocalPauli_sum line 30
  7. theorem OAI.ContinuumCoulomb.qmaLocalPauli_odd_zero line 40
  8. theorem OAI.ContinuumCoulomb.qmaLocalEvenPauli_sum line 49
  9. theorem OAI.ContinuumCoulomb.qmaLocalEvenPauli_count line 64
  10. theorem OAI.ContinuumCoulomb.qmaLocalEvenPauli_support line 76
  11. theorem OAI.ContinuumCoulomb.qmaLocalEvenPauli_even line 82