OAI/MathematicalPhysics/PEPSMove/EntropyContinuity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.posSemidef_zero_of_trace_re_zero line 15
2. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_abs_le_homogeneous line 32
3. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceDistance line 53
4. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceDistance_parts line 55
5. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_continuity line 70
6. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.hsEnergy line 115
7. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.hsEnergy_nonneg line 118
8. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.hsEnergy_trace line 122
9. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.hsEnergy_unitary_left line 127
10. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceDistance_spectral line 139
11. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.norm_sq_sub_norm_sq_le line 149
12. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceDistance_gram_squared line 162
13. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_one_add_le_two_sqrt line 235
14. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.mixing_modulus_le line 246
15. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceDistance_nonneg line 271
16. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_gram_modulus line 279