OAI/MathematicalPhysics/PEPSSubvolume/EntropyHolder.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Pinching entropy, trace Holder and single-filter lower bounds.

  1. def OAI.PolynomialPEPS.Subvolume.MatrixEntropy.entropy line 28
  2. theorem OAI.PolynomialPEPS.Subvolume.MatrixEntropy.unitary_row_normSq line 31
  3. theorem OAI.PolynomialPEPS.Subvolume.MatrixEntropy.unitary_col_normSq line 37
  4. theorem OAI.PolynomialPEPS.Subvolume.MatrixEntropy.diagonal_conjugate line 43
  5. theorem OAI.PolynomialPEPS.Subvolume.MatrixEntropy.entropy_le_diagonal line 54
  6. theorem OAI.PolynomialPEPS.Subvolume.SpectralHolder.diagonal_rpow_le line 85
  7. theorem OAI.PolynomialPEPS.Subvolume.SpectralHolder.eigenvalues_unitary_conjugate line 106
  8. theorem OAI.PolynomialPEPS.Subvolume.SpectralHolder.trace_spectral_pairing line 115
  9. theorem OAI.PolynomialPEPS.Subvolume.SpectralHolder.trace_square_mul_le line 124
  10. theorem OAI.PolynomialPEPS.Subvolume.PrefixLower.filter_norm_sq_trace line 169
  11. theorem OAI.PolynomialPEPS.Subvolume.PrefixLower.single_filter_moment line 183
  12. theorem OAI.PolynomialPEPS.Subvolume.trace_reducedDensity line 207
  13. theorem OAI.PolynomialPEPS.Subvolume.marginal_eigenvalues_sum line 211
  14. theorem OAI.PolynomialPEPS.Subvolume.GroundMGF.single_filter_entropy line 227