OAI/LinearAlgebra/MatrixMultiplication/FieldParameters/Contractions.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Fixed rational distributions and their entropy and capacity formulas.

  1. abbrev OAI.MatrixMultiplication.AllFieldParameters.Contractions.Ref line 13
  2. abbrev OAI.MatrixMultiplication.AllFieldParameters.Contractions.Law line 14
  3. structure OAI.MatrixMultiplication.AllFieldParameters.Contractions.BuildState line 18
  4. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.BuildState.program line 24
  5. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.opKey line 26
  6. abbrev OAI.MatrixMultiplication.AllFieldParameters.Contractions.Build line 34
  7. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.emit line 36
  8. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.lit line 48
  9. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.add line 50
  10. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.neg line 53
  11. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.sub line 55
  12. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.mul line 57
  13. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.inv line 61
  14. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.divide line 63
  15. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.log line 65
  16. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.powerAux line 68
  17. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.power line 76
  18. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.sumRefs line 78
  19. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.getLaw line 80
  20. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.addMass line 83
  21. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.normalize line 90
  22. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.entropy line 94
  23. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildWeight line 100
  24. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.insertInteger line 106
  25. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.sortIntegers line 110
  26. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.weightArguments line 114
  27. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildWeights line 117
  28. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.initialMultiplicity line 120
  29. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildInitial line 123
  30. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildSplit line 132
  31. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.getSplit line 141
  32. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildBinary line 144
  33. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildZeroPairs line 148
  34. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.getPairs line 155
  35. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.littleLaw line 158
  36. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.pair line 168
  37. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.maxAxis line 180
  38. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildHalfLaws line 183
  39. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.getHalf line 199
  40. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.orders line 203
  41. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.priority line 206
  42. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.capacity line 211
  43. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.sortShape line 244
  44. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.secondTypes line 249
  45. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildMasses line 252
  46. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildLittleMasses line 259
  47. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.addRow line 268
  48. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.rowTotals line 276
  49. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.binaryEntropy line 279
  50. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.coefficientStep line 282
  51. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.coefficients line 287
  52. structure OAI.MatrixMultiplication.AllFieldParameters.Contractions.Roots line 289
  53. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.buildAll line 322
  54. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.built line 428
  55. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.program line 430
  56. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.roots line 432
  57. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.exponent line 434
  58. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.scalar line 436
  59. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.Y line 438
  60. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.S line 440
  61. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.R line 442
  62. def OAI.MatrixMultiplication.AllFieldParameters.Contractions.ratio line 444