OAI/MathematicalPhysics/PEPSSubvolume/SSARegularized.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Partial trace identities and singular strong subadditivity limits.

  1. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR line 29
  2. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL line 31
  3. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.insR line 33
  4. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.insR_isometry line 35
  5. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_compression line 39
  6. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_posSemidef line 44
  7. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_posDef line 49
  8. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.trace_ptrR line 56
  9. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_dual line 59
  10. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL_dual line 65
  11. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_kronecker line 75
  12. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_add line 81
  13. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_smul line 85
  14. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_one line 89
  15. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.traceEntropy line 100
  16. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.trace_cfc line 102
  17. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.traceEntropy_spectral line 109
  18. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.traceEntropy_log line 113
  19. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.entropy_regularization_continuous line 122
  20. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.reindexHom line 146
  21. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.reindexHom_posDef line 150
  22. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.reindexHom_posSemidef line 153
  23. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.reindexHom_trace line 156
  24. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_reindexHom line 161
  25. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.entropy_reindexHom line 168
  26. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL_eq_swap line 177
  27. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL_posSemidef line 180
  28. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL_posDef line 185
  29. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL_add line 191
  30. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL_smul line 195
  31. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL_one line 199
  32. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.reindexHom_symm_apply line 211
  33. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.trace_mul_reindexHom line 216
  34. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.assocMatrix line 220
  35. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.liftBC line 223
  36. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrR_liftBC line 226
  37. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_tensorRight line 235
  38. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_liftBC line 241
  39. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.trace_liftBC_dual line 247
  40. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.ptrL_ptrR_assoc line 253
  41. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.strong_subadditivity_posDef line 259
  42. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.reindexHom_smul_real line 290
  43. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.assocMatrix_regularize line 293
  44. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.strong_subadditivity line 297