OAI/LinearAlgebra/MatrixMultiplication/FieldParameters/Compatibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed rational distributions and their entropy and capacity formulas.

  1. def OAI.MatrixMultiplication.AllFieldParameters.statisticLaw line 10
  2. def OAI.MatrixMultiplication.AllFieldParameters.statisticComplement line 15
  3. theorem OAI.MatrixMultiplication.AllFieldParameters.statisticLaw_complement line 17
  4. theorem OAI.MatrixMultiplication.AllFieldParameters.statisticLaw_outside_support line 21
  5. theorem OAI.MatrixMultiplication.AllFieldParameters.littleLaw_eq_statisticLaw line 26
  6. theorem OAI.MatrixMultiplication.AllFieldParameters.littleLaw_outside_support line 29
  7. theorem OAI.MatrixMultiplication.AllFieldParameters.littleLaw_complement line 33
  8. theorem OAI.MatrixMultiplication.AllFieldParameters.child_statistic_weight_bounded line 44
  9. theorem OAI.MatrixMultiplication.AllFieldParameters.pair_complement_involution line 47