OAI/LinearAlgebra/MatrixMultiplication/FieldParameters/Entropy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed rational distributions and their entropy and capacity formulas.

  1. def OAI.MatrixMultiplication.AllFieldParameters.homogeneousEntropy line 15
  2. theorem OAI.MatrixMultiplication.AllFieldParameters.homogeneousEntropy_normalized line 18
  3. theorem OAI.MatrixMultiplication.AllFieldParameters.entropyTerm_divide line 23
  4. theorem OAI.MatrixMultiplication.AllFieldParameters.homogeneousEntropy_eq_mass_mul line 33
  5. theorem OAI.MatrixMultiplication.AllFieldParameters.homogeneousEntropy_zero line 44
  6. theorem OAI.MatrixMultiplication.AllFieldParameters.homogeneousEntropy_expansion line 48