OAI/LinearAlgebra/MatrixMultiplication/FieldParameters/Basic.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Fixed rational distributions and their entropy and capacity formulas.

  1. abbrev OAI.MatrixMultiplication.AllFieldParameters.Shape line 11
  2. def OAI.MatrixMultiplication.AllFieldParameters.shape line 13
  3. def OAI.MatrixMultiplication.AllFieldParameters.shapes line 15
  4. def OAI.MatrixMultiplication.AllFieldParameters.positive line 19
  5. def OAI.MatrixMultiplication.AllFieldParameters.sorted line 21
  6. def OAI.MatrixMultiplication.AllFieldParameters.sortedInitial line 23
  7. def OAI.MatrixMultiplication.AllFieldParameters.positiveInitial line 25
  8. def OAI.MatrixMultiplication.AllFieldParameters.positiveSecond line 27
  9. def OAI.MatrixMultiplication.AllFieldParameters.zeroSecond line 29
  10. def OAI.MatrixMultiplication.AllFieldParameters.shapeMax line 31
  11. def OAI.MatrixMultiplication.AllFieldParameters.below line 33
  12. def OAI.MatrixMultiplication.AllFieldParameters.complement line 37
  13. def OAI.MatrixMultiplication.AllFieldParameters.tablea line 39
  14. def OAI.MatrixMultiplication.AllFieldParameters.tableP line 43
  15. def OAI.MatrixMultiplication.AllFieldParameters.tablep line 57
  16. def OAI.MatrixMultiplication.AllFieldParameters.tabled line 65
  17. def OAI.MatrixMultiplication.AllFieldParameters.tablez line 75
  18. theorem OAI.MatrixMultiplication.AllFieldParameters.table_lengths line 81
  19. theorem OAI.MatrixMultiplication.AllFieldParameters.parent_counts line 85
  20. def OAI.MatrixMultiplication.AllFieldParameters.statisticWeight line 89
  21. def OAI.MatrixMultiplication.AllFieldParameters.multiplicity line 91
  22. def OAI.MatrixMultiplication.AllFieldParameters.kappa line 93
  23. theorem OAI.MatrixMultiplication.AllFieldParameters.kappa_involution line 95
  24. theorem OAI.MatrixMultiplication.AllFieldParameters.multiplicity_kappa line 99
  25. theorem OAI.MatrixMultiplication.AllFieldParameters.statisticWeight_kappa line 103
  26. def OAI.MatrixMultiplication.AllFieldParameters.weight line 108
  27. theorem OAI.MatrixMultiplication.AllFieldParameters.weight_nonnegative line 111
  28. abbrev OAI.MatrixMultiplication.AllFieldParameters.SplitKey line 115
  29. def OAI.MatrixMultiplication.AllFieldParameters.splitKeys line 117
  30. def OAI.MatrixMultiplication.AllFieldParameters.assigned line 123
  31. def OAI.MatrixMultiplication.AllFieldParameters.splitSignature line 126
  32. def OAI.MatrixMultiplication.AllFieldParameters.stageASignature line 129
  33. def OAI.MatrixMultiplication.AllFieldParameters.stageBSignature line 131
  34. def OAI.MatrixMultiplication.AllFieldParameters.splitWeight line 133
  35. def OAI.MatrixMultiplication.AllFieldParameters.splitLaw line 136
  36. def OAI.MatrixMultiplication.AllFieldParameters.stageALaw line 141
  37. def OAI.MatrixMultiplication.AllFieldParameters.stageBLaw line 143
  38. theorem OAI.MatrixMultiplication.AllFieldParameters.split_consumption line 145
  39. theorem OAI.MatrixMultiplication.AllFieldParameters.splitSignature_complement line 149
  40. theorem OAI.MatrixMultiplication.AllFieldParameters.splitWeight_complement line 155
  41. theorem OAI.MatrixMultiplication.AllFieldParameters.splitLaw_complement line 160
  42. theorem OAI.MatrixMultiplication.AllFieldParameters.splitLaw_outside_support line 166
  43. def OAI.MatrixMultiplication.AllFieldParameters.binaryKeys line 170
  44. def OAI.MatrixMultiplication.AllFieldParameters.binaryInteger line 174
  45. def OAI.MatrixMultiplication.AllFieldParameters.binaryParameter line 176
  46. theorem OAI.MatrixMultiplication.AllFieldParameters.binary_consumption line 178
  47. theorem OAI.MatrixMultiplication.AllFieldParameters.binary_table_range line 180
  48. theorem OAI.MatrixMultiplication.AllFieldParameters.complementary_binary_parameters_are_distinct line 183
  49. theorem OAI.MatrixMultiplication.AllFieldParameters.unreachable_parent_retained line 187
  50. abbrev OAI.MatrixMultiplication.AllFieldParameters.PairSlot line 189
  51. def OAI.MatrixMultiplication.AllFieldParameters.unorderedPairs line 191
  52. def OAI.MatrixMultiplication.AllFieldParameters.pairKeys line 197
  53. def OAI.MatrixMultiplication.AllFieldParameters.orderedPairInteger line 201
  54. def OAI.MatrixMultiplication.AllFieldParameters.orderedPairs line 204
  55. def OAI.MatrixMultiplication.AllFieldParameters.zeroPairLaw line 209
  56. theorem OAI.MatrixMultiplication.AllFieldParameters.pair_consumption line 215
  57. theorem OAI.MatrixMultiplication.AllFieldParameters.orderedPairInteger_swap line 217
  58. theorem OAI.MatrixMultiplication.AllFieldParameters.zeroPairLaw_swap line 221
  59. theorem OAI.MatrixMultiplication.AllFieldParameters.zeroPairLaw_outside_support line 225