OAI/MathematicalPhysics/PEPSSubvolume/QuantumSSA.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Matrix relative entropy and strong subadditivity inequalities.

  1. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.cfc_intertwine line 27
  2. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.compression_mono line 73
  3. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.isometry_mulVec_injective line 80
  4. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_compression line 86
  5. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.tensorLeftHom line 136
  6. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.tensorRightHom line 148
  7. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_mul_of_posDef line 160
  8. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_kronecker line 169
  9. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.conjMatrixHom line 197
  10. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_transpose line 201
  11. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_inv line 216
  12. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.vecLE line 223
  13. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.modular line 231
  14. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.modular_posDef line 233
  15. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.modular_mulVec line 236
  16. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.log_modular_mulVec line 240
  17. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.sqrt_posDef line 249
  18. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.sqrt_square line 252
  19. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.modular_log_pairing line 255
  20. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.eq_of_vec_pairing line 264
  21. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.pairing_compression line 272
  22. def OAI.PolynomialPEPS.Subvolume.QuantumSSA.petzEmbedding line 276
  23. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.petzEmbedding_mulVec line 282
  24. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.posDef_mul_inv line 288
  25. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.posDef_inv_mul line 290
  26. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.sqrt_inv_sandwich line 293
  27. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.inv_sqrt_square line 299
  28. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.sqrt_sandwich_inv line 302
  29. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.hs_petz_pairing line 307
  30. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.petzEmbedding_isometry line 335
  31. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.hs_petz_modular line 347
  32. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.petzEmbedding_modular line 379
  33. lemma OAI.PolynomialPEPS.Subvolume.QuantumSSA.petzEmbedding_sqrt line 389
  34. theorem OAI.PolynomialPEPS.Subvolume.QuantumSSA.relative_entropy_mono_posDef line 394