OAI/MathematicalPhysics/PEPSMove/ModularDistance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsEnergy_same_gram line 18
2. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsEnergy_add_two line 26
3. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsEnergy_unitary_right line 37
4. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.power_conjugation line 47
5. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.phase_conjugation line 52
6. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.phase_neg line 58
7. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.trace_conjugation line 66
8. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.modular_state_distance line 77