OAI/MathematicalPhysics/PEPSSubvolume/EntropyDimension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dimension bounds for finite-state entropy.

  1. theorem OAI.PolynomialPEPS.Subvolume.vonNeumannEntropy_nonneg line 28
  2. theorem OAI.PolynomialPEPS.Subvolume.vonNeumannEntropy_empty line 37
  3. theorem OAI.PolynomialPEPS.SubvolumeEntropy.sum_negMulLog_le_log_card line 53
  4. theorem OAI.PolynomialPEPS.Subvolume.vonNeumannEntropy_le_card_log line 79