OAI/MathematicalPhysics/PEPSMove/MoveBounds.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PolynomialPEPS.PhysicalMove.LocalMove.quartic_loss_absorptionline 12 - theorem
OAI.PolynomialPEPS.PhysicalMove.LocalMove.entropy_loss_absorptionline 51 - theorem
OAI.PolynomialPEPS.PhysicalMove.LocalMove.entropy_remainder_boundline 89 - theorem
OAI.PolynomialPEPS.PhysicalMove.LocalMove.phase_majorantline 104 - theorem
OAI.PolynomialPEPS.PhysicalMove.LocalMove.modular_remainder_majorantline 113