OAI/MathematicalPhysics/PEPSMove/UnitaryCovariance.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.reshuffle_local_rotate line 18
  2. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.tensorRightUnitary line 38
  3. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.tensorLeftUnitary line 48
  4. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.transposeUnitary line 58
  5. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_rotate line 70
  6. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.entropy_unitary_conj line 87
  7. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.gram_unitary_right line 108
  8. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.gram_unitary_rotate line 114
  9. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.hsEnergy_unitary_rotate line 122
  10. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_gram_rotate line 127
  11. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.power_left_unitary line 141
  12. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.tensorRight_diagonal line 145
  13. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.tensorRight_power line 154
  14. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.filtered_unitary_covariance line 168
  15. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.flatten_norm_unitary_rotate line 189
  16. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.one_copy_move_unitary_image line 203
  17. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.tensorRightUnitary_star line 265
  18. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.tensorLeftUnitary_star line 271
  19. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.transposeUnitary_star line 276
  20. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.undo_unitary_rotate line 281
  21. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_gram_rotate line 290
  22. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.spectral_diagonalize line 300
  23. theorem OAI.PolynomialPEPS.PhysicalMove.LocalMove.one_copy_move_cfc line 324