OAI/MathematicalPhysics/PEPSMove/PartialTrace.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR line 15
  2. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL line 17
  3. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.insR line 19
  4. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.insR_isometry line 21
  5. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_compression line 25
  6. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_posSemidef line 30
  7. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_posDef line 35
  8. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.trace_ptrR line 42
  9. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_dual line 45
  10. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_dual line 51
  11. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_kronecker line 61
  12. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_add line 67
  13. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_smul line 71
  14. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_one line 75
  15. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy line 86
  16. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.trace_cfc line 88
  17. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_spectral line 95
  18. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_log line 99
  19. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.entropy_regularization_continuous line 110
  20. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.reindexHom line 134
  21. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.reindexHom_posDef line 138
  22. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.reindexHom_posSemidef line 141
  23. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.reindexHom_trace line 144
  24. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_reindexHom line 149
  25. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.entropy_reindexHom line 156
  26. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_eq_swap line 165
  27. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_posSemidef line 168
  28. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_posDef line 173
  29. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_add line 179
  30. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_smul line 183
  31. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_one line 187