OAI/MathematicalPhysics/PEPSMove/EntropyHolder.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialPEPS.PhysicalMove.MatrixEntropy.entropy line 14
  2. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixEntropy.unitary_row_normSq line 17
  3. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixEntropy.unitary_col_normSq line 23
  4. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixEntropy.diagonal_conjugate line 29
  5. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixEntropy.entropy_le_diagonal line 42
  6. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralHolder.diagonal_rpow_le line 74
  7. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralHolder.eigenvalues_unitary_conjugate line 95
  8. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralHolder.trace_spectral_pairing line 104
  9. theorem OAI.PolynomialPEPS.PhysicalMove.SpectralHolder.trace_square_mul_le line 115
  10. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.gramMoment_conjTranspose line 161
  11. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.trace_power_gram_le line 174
  12. theorem OAI.PolynomialPEPS.PhysicalMove.MatrixInterpolation.one_filter_petz_bound line 221