OAI/MathematicalPhysics/PEPSMove/BoundaryEnergy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.phase_mul_power line 15
2. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.power_mul_phase line 29
3. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.power_imag_phase line 43
4. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsEnergy_imaginary_contraction line 56
5. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.hsEnergy_left_real_power line 79
6. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.paired_entropy_boundary line 107
7. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.coefficient_kernel line 203
8. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.imaginary_marginal_on_coefficient line 211
9. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.hsEnergy_phase_real line 227
10. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.one_filter_with_marginal_phase line 233
11. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.left_boundary_trace line 268
12. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.right_boundary_entropy line 306
13. theorem OAI.PolynomialPEPS.PhysicalMove.ConditionalCollision.boundary_pair_energy line 345