OAI/LinearAlgebra/MatrixMultiplication/FieldParameters/HalfComplement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Fixed rational distributions and their entropy and capacity formulas.

  1. theorem OAI.MatrixMultiplication.AllFieldParameters.normalized_singleton_law line 11
  2. theorem OAI.MatrixMultiplication.AllFieldParameters.pairWeight_zero line 25
  3. theorem OAI.MatrixMultiplication.AllFieldParameters.pairWeight_eight line 28
  4. theorem OAI.MatrixMultiplication.AllFieldParameters.pairKappa_zero line 31
  5. theorem OAI.MatrixMultiplication.AllFieldParameters.pairKappa_eight line 34
  6. theorem OAI.MatrixMultiplication.AllFieldParameters.halfLaw_weight_zero line 37
  7. theorem OAI.MatrixMultiplication.AllFieldParameters.halfLaw_weight_eight line 46
  8. theorem OAI.MatrixMultiplication.AllFieldParameters.complementary_half_sides_zero_parent line 55
  9. theorem OAI.MatrixMultiplication.AllFieldParameters.halfLaw_complementary_sides line 58
  10. theorem OAI.MatrixMultiplication.AllFieldParameters.zero_maximum_axis_nonzero line 72
  11. theorem OAI.MatrixMultiplication.AllFieldParameters.halfLaw_at_maximum line 75
  12. theorem OAI.MatrixMultiplication.AllFieldParameters.zeroPairLaw_shapeMax_eight line 81