OAI/MathematicalPhysics/PEPSMove/StrongSubadditivity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.reindexHom_symm_apply line 16
2. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.trace_mul_reindexHom line 21
3. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.assocMatrix line 25
4. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.liftBC line 28
5. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_liftBC line 31
6. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_tensorRight line 40
7. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_liftBC line 46
8. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.trace_liftBC_dual line 52
9. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_ptrR_assoc line 58
10. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.strong_subadditivity_posDef line 66
11. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.reindexHom_smul_real line 97
12. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.assocMatrix_regularize line 100
13. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.strong_subadditivity line 106