OAI/MathematicalPhysics/PEPSMove/PhaseTransfer.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialPEPS.PhysicalMove.SpectralCurve.curve line 15
2. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralCurve.curve_zero line 18
3. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralCurve.curve_add line 24
4. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralCurve.curve_star line 29
5. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralCurve.curve_mem_unitary line 36
6. def OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.phase line 50
7. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.phase_apply line 55
8. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.spectralHom_conjugate line 64
9. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.root_gram line 71
10. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.phase_root_deficit line 79
11. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_neg line 139
12. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_sub_comm line 143
13. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_add_three line 147
14. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsSquare_unitary_sub line 163
15. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.phase_transfer line 184