OAI/MathematicalPhysics/PEPSMove/LogCompression.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.cfc_intertwine line 15
  2. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.compression_mono line 61
  3. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.isometry_mulVec_injective line 68
  4. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_compression line 77
  5. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.tensorLeftHom line 127
  6. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.tensorRightHom line 139
  7. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_mul_of_posDef line 151
  8. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_kronecker line 160
  9. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conjMatrixHom line 188
  10. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_transpose line 192
  11. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_inv line 207
  12. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.vecLE line 214
  13. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.modular line 223
  14. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.modular_posDef line 225
  15. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.modular_mulVec line 228
  16. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.log_modular_mulVec line 232
  17. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.sqrt_posDef line 241
  18. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.sqrt_square line 244
  19. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.modular_log_pairing line 247
  20. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.eq_of_vec_pairing line 256
  21. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.pairing_compression line 264
  22. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.petzEmbedding line 269
  23. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.petzEmbedding_mulVec line 275
  24. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.posDef_mul_inv line 281
  25. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.posDef_inv_mul line 283
  26. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.sqrt_inv_sandwich line 286
  27. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.inv_sqrt_square line 292
  28. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.sqrt_sandwich_inv line 295
  29. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.hs_petz_pairing line 300
  30. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.petzEmbedding_isometry line 328
  31. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.hs_petz_modular line 340
  32. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.petzEmbedding_modular line 372
  33. lemma OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.petzEmbedding_sqrt line 382
  34. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.relative_entropy_mono_posDef line 389