OAI/LinearAlgebra/MatrixMultiplication/FieldParameters/Distributions.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Fixed rational distributions and their entropy and capacity formulas.

  1. def OAI.MatrixMultiplication.AllFieldParameters.initialMultiplicity line 11
  2. def OAI.MatrixMultiplication.AllFieldParameters.initialInteger line 14
  3. def OAI.MatrixMultiplication.AllFieldParameters.initialWeight line 16
  4. def OAI.MatrixMultiplication.AllFieldParameters.initialLaw line 19
  5. theorem OAI.MatrixMultiplication.AllFieldParameters.initial_table_arguments_bounded line 22
  6. theorem OAI.MatrixMultiplication.AllFieldParameters.initialWeight_positive line 24
  7. theorem OAI.MatrixMultiplication.AllFieldParameters.initialLaw_positive line 33
  8. theorem OAI.MatrixMultiplication.AllFieldParameters.initialLaw_normalized line 38
  9. theorem OAI.MatrixMultiplication.AllFieldParameters.binary_table_bounds line 48
  10. theorem OAI.MatrixMultiplication.AllFieldParameters.binaryInteger_bounds line 50
  11. theorem OAI.MatrixMultiplication.AllFieldParameters.binaryParameter_bounds line 58
  12. def OAI.MatrixMultiplication.AllFieldParameters.singletonSlot line 68
  13. def OAI.MatrixMultiplication.AllFieldParameters.littleLaw line 76
  14. theorem OAI.MatrixMultiplication.AllFieldParameters.littleLaw_nonnegative line 81
  15. theorem OAI.MatrixMultiplication.AllFieldParameters.littleLaw_normalized line 87
  16. theorem OAI.MatrixMultiplication.AllFieldParameters.orderedPairWeight_positive line 103
  17. theorem OAI.MatrixMultiplication.AllFieldParameters.orderedPairs_nonempty line 108
  18. theorem OAI.MatrixMultiplication.AllFieldParameters.orderedPairs_support line 110
  19. theorem OAI.MatrixMultiplication.AllFieldParameters.zeroPairLaw_positive line 118
  20. theorem OAI.MatrixMultiplication.AllFieldParameters.zeroPairLaw_normalized line 125