OAI/LinearAlgebra/MatrixFields/Tensors/CWCompleteStatistics.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCoefficientExtraction.coeff_triple line 22
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCoefficientExtraction.rankAtMost_coeff line 59
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCoefficientExtraction.rank_power line 81
  4. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.zeroForm line 110
  5. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.interiorForm line 112
  6. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.lastForm line 115
  7. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.interiorSum line 117
  8. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.tensor line 119
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.interior_pair_sum line 129
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.tensor_zero_side line 160
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.tensor_cyclic line 180
  12. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.form line 198
  13. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.left line 200
  14. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.other line 205
  15. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.polynomial line 210
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.rank_bound line 213
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.polynomial_apply line 219
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.coeff_mul_two line 233
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.coeff_mul_three line 239
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.vanishes line 245
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.leading line 257
  22. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.degreeBound line 269
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.degree_bound line 273
  24. def OAI.MatrixAllFields.MatrixMultiplication.FieldCW.approximation line 285
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.FieldCW.rank_power line 293
  26. def OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.lastLabel line 308
  27. def OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.complement line 310
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.complement_zero line 313
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.complement_last line 316
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.complement_involution line 319
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.complement_interior line 323
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.zero_support_iff line 331
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.tensor_zero_matching line 366
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.tensor_middle_zero_matching line 372
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.tensor_last_zero_matching line 379
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.zeroX_leaf line 386
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.zeroY_leaf line 396
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafRestrictions.zeroZ_leaf line 408
  39. def OAI.MatrixAllFields.MatrixMultiplication.CWLeafStatistics.weight line 430
  40. def OAI.MatrixAllFields.MatrixMultiplication.CWLeafStatistics.pairStatistic line 432
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafStatistics.statistic_weight line 439
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafStatistics.pair_multiplicity line 443
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafStatistics.complement_weight line 448
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafStatistics.complement_statistic line 452
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.CWLeafStatistics.ordered_pair_multiplicity line 458
  46. def OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.wordWeight line 485
  47. def OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.wordComplement line 487
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.wordComplement_involution line 490
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.weight_eq_zero_iff line 495
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.wordWeight_zero line 498
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.site_nonzero line 508
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.zeroX_word_match line 516
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.zeroY_word_match line 534
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.zeroZ_word_match line 552
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompatibilityTransfer.transfer_window line 570
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStrands.site_weight_support line 599
  57. def OAI.MatrixAllFields.MatrixMultiplication.CWStrands.weight line 635
  58. def OAI.MatrixAllFields.MatrixMultiplication.CWStrands.strand line 638
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStrands.strand_support line 641
  60. def OAI.MatrixAllFields.MatrixMultiplication.CWStrands.shapeTensor line 654
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStrands.shapeTensor_support line 659
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStrands.weight_sum_elim line 667
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStrands.strand_sum_elim line 672
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStrands.shape_split line 680
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStrands.shape_split_sub line 700
  66. def OAI.MatrixAllFields.MatrixMultiplication.CWStrands.splitMatrix line 714
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.CWStrands.shape_split_restrict line 719
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCoarseIndices.label_weight_le_two line 748
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCoarseIndices.weight_le line 751
  70. def OAI.MatrixAllFields.MatrixMultiplication.CWCoarseIndices.coarseIndex line 757
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCoarseIndices.strand_coarse_support line 760
  72. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCoarseIndices.split_coarse_support line 766
  73. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.Left line 816
  74. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.Right line 817
  75. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.shapeNat line 819
  76. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.parentTensor line 821
  77. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.coarse line 828
  78. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.leftTensor line 831
  79. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.rightTensor line 835
  80. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.block_eq_product line 840
  81. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.canonicalBase_eq_children line 859
  82. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.RawStrands line 887
  83. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.rawParentSource line 890
  84. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.joinWords line 894
  85. def OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.joinMatrix line 898
  86. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCanonicalCW.parentTensor_restrict line 902
  87. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapeLeaves.complement_word_weight line 925
  88. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapeLeaves.zeroX_shape_leaf line 934
  89. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapeLeaves.zeroY_shape_leaf line 955
  90. theorem OAI.MatrixAllFields.MatrixMultiplication.CWShapeLeaves.zeroZ_shape_leaf line 976
  91. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.Raw line 1011
  92. abbrev OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.Alphabet line 1012
  93. def OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.complementWord line 1014
  94. def OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroWord line 1015
  95. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroX_local line 1019
  96. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroY_local line 1029
  97. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroZ_local line 1040
  98. def OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.rawSelected line 1055
  99. def OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.complementarySelected line 1058
  100. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroX_class line 1064
  101. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroY_class line 1076
  102. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroZ_class line 1088
  103. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroX_masked line 1100
  104. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroY_masked line 1116
  105. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroZ_masked line 1132
  106. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroX_restriction line 1148
  107. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroY_restriction line 1166
  108. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zeroZ_restriction line 1184
  109. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.exact_selected_window line 1207
  110. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.exact_complementary_window line 1214
  111. theorem OAI.MatrixAllFields.MatrixMultiplication.CWWindowedLeaves.zero_window line 1230
  112. def OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.pairEquiv line 1255
  113. def OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.orderedEquiv line 1261
  114. def OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.twoStatistic line 1267
  115. def OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.fourStatistic line 1268
  116. def OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.complementStatistic line 1271
  117. def OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.orderedComplementStatistic line 1277
  118. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.two_weight line 1280
  119. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.four_weight line 1285
  120. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.two_multiplicity line 1291
  121. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.four_multiplicity line 1301
  122. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.two_complement line 1317
  123. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.four_complement line 1321
  124. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.two_fixedWeight_multiplicity line 1327
  125. theorem OAI.MatrixAllFields.MatrixMultiplication.CWCompleteStatistics.four_fixedWeight_multiplicity line 1333