OAI/MathematicalPhysics/PEPSMove/PureEntropy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialPEPS.PhysicalMove.PureEntropy.sum_eigen_stat_mul_comm line 17
2. theorem OAI.PolynomialPEPS.PhysicalMove.PureEntropy.sum_eigen_stat_transpose line 37
3. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_transpose line 54
4. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_gram line 59
5. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.purifyingSwap line 67
6. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.swap_gram_left line 71
7. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.swap_gram_right line 84
8. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.swap_gram_kept line 97
9. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.entropy_triangle line 105
10. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_lower line 129
11. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_abs_le line 138