OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QubitSubdivisionReal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The selected phases make every subdivision output term a real matrix.

  1. theorem OAI.ContinuumCoulomb.QMAEntryParity.sum line 14
  2. theorem OAI.ContinuumCoulomb.qmaIdentity_real line 28
  3. theorem OAI.ContinuumCoulomb.QMAEntryParity.kronecker line 33
  4. theorem OAI.ContinuumCoulomb.QMAEntryParity.submatrix line 39
  5. theorem OAI.ContinuumCoulomb.qmaOccupation_real line 46
  6. theorem OAI.ContinuumCoulomb.qmaJoinMatrix_real line 54
  7. theorem OAI.ContinuumCoulomb.qmaPolarizedJoin_real line 61
  8. theorem OAI.ContinuumCoulomb.qmaSubdivisionLocalPiece_real line 68
  9. theorem OAI.ContinuumCoulomb.qmaSubdivisionLocalFamily_real line 79
  10. theorem OAI.ContinuumCoulomb.qmaSubdivisionOnQubits_real line 90