OAI/LinearAlgebra/MatrixFields/Parameters/ParametersWeights.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.Shape line 13
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.shape line 15
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.shapes line 17
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.positive line 21
  5. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.sorted line 23
  6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.sortedInitial line 25
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.positiveInitial line 27
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.positiveSecond line 29
  9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zeroSecond line 31
  10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.shapeMax line 33
  11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.below line 35
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.complement line 39
  13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.tablea line 41
  14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.tableP line 45
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.tablep line 59
  16. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.tabled line 67
  17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.tablez line 77
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.table_lengths line 83
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.parent_counts line 87
  20. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticWeight line 91
  21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.multiplicity line 93
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.kappa line 95
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.kappa_involution line 97
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.multiplicity_kappa line 101
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticWeight_kappa line 105
  26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.weight line 110
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.weight_nonnegative line 113
  28. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.SplitKey line 117
  29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitKeys line 119
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.assigned line 125
  31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitSignature line 128
  32. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageASignature line 131
  33. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageBSignature line 133
  34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitWeight line 135
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitLaw line 138
  36. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageALaw line 143
  37. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageBLaw line 145
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.split_consumption line 147
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitSignature_complement line 151
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitWeight_complement line 157
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitLaw_complement line 162
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitLaw_outside_support line 168
  43. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binaryKeys line 172
  44. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binaryInteger line 176
  45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binaryParameter line 178
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binary_consumption line 180
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binary_table_range line 182
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.complementary_binary_parameters_are_distinct line 185
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.unreachable_parent_retained line 189
  50. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.PairSlot line 191
  51. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.unorderedPairs line 193
  52. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.pairKeys line 199
  53. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.orderedPairInteger line 203
  54. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.orderedPairs line 206
  55. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zeroPairLaw line 211
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.pair_consumption line 217
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.orderedPairInteger_swap line 219
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zeroPairLaw_swap line 223
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zeroPairLaw_outside_support line 227
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.truncated_polynomial_positive line 232
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.weight_positive_of_argument_bound line 256
  62. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.weightArguments line 266
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.all_weight_arguments_bounded line 268
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.all_weights_positive line 271
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.normalized_sum line 274
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.normalized_positive line 279