OAI/MathematicalPhysics/PEPSMove/EntropyBounds.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.block_posSemidef line 15
  2. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_block line 31
  3. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.flagEquiv line 47
  4. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.flag line 53
  5. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.flag_apply line 56
  6. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.flag_posSemidef line 60
  7. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_flag line 63
  8. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrR_flag line 67
  9. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.ptrL_assoc_flag line 72
  10. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_superadditive line 81
  11. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.trace_real_spectral line 97
  12. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_smul_real line 104
  13. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.trace_mul_mono_right line 114
  14. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_add_le_posDef line 127
  15. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.traceEntropy_add_le line 140
  16. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.trace_ptrL line 171
  17. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.singleton_entropy line 175
  18. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.entropy_homogeneous_concave line 182
  19. def OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditionalEntropy line 205
  20. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditionalEntropy_smul line 208
  21. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_add_lower line 214
  22. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_add_upper line 219
  23. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_mixture_upper line 232
  24. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.entropy_subadditive line 252
  25. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.entropy_density_upper line 273
  26. theorem OAI.PolynomialPEPS.PhysicalMove.QuantumSSA.conditional_upper line 300