OAI/LinearAlgebra/MatrixMultiplication/FieldParameters/Laws.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Fixed rational distributions and their entropy and capacity formulas.

  1. theorem OAI.MatrixMultiplication.AllFieldParameters.assigned_mem_or_zero line 11
  2. theorem OAI.MatrixMultiplication.AllFieldParameters.assigned_argument_bound line 20
  3. theorem OAI.MatrixMultiplication.AllFieldParameters.splitWeight_positive line 26
  4. theorem OAI.MatrixMultiplication.AllFieldParameters.list_sum_map_nonnegative line 34
  5. theorem OAI.MatrixMultiplication.AllFieldParameters.list_sum_map_positive line 42
  6. theorem OAI.MatrixMultiplication.AllFieldParameters.list_sum_map_div line 51
  7. theorem OAI.MatrixMultiplication.AllFieldParameters.splitLaw_positive line 57
  8. theorem OAI.MatrixMultiplication.AllFieldParameters.splitLaw_normalized line 68
  9. theorem OAI.MatrixMultiplication.AllFieldParameters.stageA_table_arguments_bounded line 81
  10. theorem OAI.MatrixMultiplication.AllFieldParameters.stageB_table_arguments_bounded line 83
  11. theorem OAI.MatrixMultiplication.AllFieldParameters.zero_table_arguments_bounded line 85
  12. theorem OAI.MatrixMultiplication.AllFieldParameters.stageA_support_nonempty line 87
  13. theorem OAI.MatrixMultiplication.AllFieldParameters.stageB_support_nonempty line 89
  14. theorem OAI.MatrixMultiplication.AllFieldParameters.stageA_support_complement line 91
  15. theorem OAI.MatrixMultiplication.AllFieldParameters.stageB_support_complement line 94
  16. theorem OAI.MatrixMultiplication.AllFieldParameters.stageALaw_positive line 97
  17. theorem OAI.MatrixMultiplication.AllFieldParameters.stageBLaw_positive line 100
  18. theorem OAI.MatrixMultiplication.AllFieldParameters.stageALaw_normalized line 103
  19. theorem OAI.MatrixMultiplication.AllFieldParameters.stageBLaw_normalized line 107
  20. theorem OAI.MatrixMultiplication.AllFieldParameters.stageALaw_complement line 111
  21. theorem OAI.MatrixMultiplication.AllFieldParameters.stageBLaw_complement line 116