OAI/LinearAlgebra/MatrixFields/Histories/InheritedMaskMargins.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.ClassWords line 25
  2. def OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.SameClassOrbit line 27
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.sameClassOrbit_iff line 31
  4. abbrev OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.Profile line 44
  5. def OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.profile line 46
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.profile_eq_iff line 51
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.card_profile line 64
  8. def OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.classProduct line 76
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.classProduct_permutation line 80
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.statisticPopulation_permutation line 92
  11. def OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.empiricalLaw line 103
  12. def OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.typeWindow line 106
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.typeWindow_permutation line 110
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.wordPopulation_equiv line 115
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.typeWindow_equiv line 121
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.weighted_window line 137
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.product_coordinate_error line 154
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.inherited_margin line 168
  19. def OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.pushforwardLaw line 201
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.pushforwardLaw_nonneg line 205
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.pushforwardLaw_le_one line 210
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.wordPopulation_statistic line 227
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.empiricalLaw_statistic line 236
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.typeWindow_mono line 243
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.typeWindow_statistic_coordinate line 249
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.InheritedMasks.typeWindow_statistic line 264
  27. def OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.completeWordPairEquiv line 297
  28. instance OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.completeWordPairFintype line 304
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.card_completeWordPair line 309
  30. def OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.pairClassProduct line 323
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.pairClassProduct_smul line 329
  32. def OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.childWindows line 351
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.childWindows_smul line 359
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.delete_invariant line 371
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.delete_used_left line 384
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.delete_used_middle line 392
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySymmetry.delete_used_right line 400
  38. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.membership line 427
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.membership_sq line 430
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.membership_nonneg line 435
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.membership_le_one line 440
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.sum_membership line 447
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.sum_perm_right line 453
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.sum_membership_position_eq line 457
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.card_mul_sum_membership line 465
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_membership line 477
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.sum_membership_mul_position_eq line 488
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.card_sub_one_mul_sum_membership_mul line 500
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_membership_mul_of_ne line 536
  50. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.matchingCount line 580
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_matchingCount line 583
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_matchingCount_sq line 591
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.matchingCount_variance line 628
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.matchingCount_variance_le line 641
  55. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.statisticPositions line 674
  56. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.statisticMatchingCount line 679
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.statisticMatchingCount_variance_le line 684
  58. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.twoHalfCount line 714
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.twoHalfCount_eq_matchingCount line 717
  60. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.relativePairEquiv line 737
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_relativePerm line 756
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_twoHalfCount line 764
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.twoHalfCount_statisticPositions line 771
  64. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.relativeFamily line 785
  65. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.relativeFamilyPairEquiv line 789
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_relativeFamily line 814
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.sum_twoHalfCount_eq_matchingCount line 825
  68. abbrev OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.ClassPermutations line 857
  69. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.populationSize line 859
  70. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingCount line 862
  71. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingMean line 866
  72. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_totalMatchingCount line 869
  73. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingMean_eq line 880
  74. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingCount_variance_le line 890
  75. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingCount_deviation_le line 905
  76. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.normalizedMatchingCount_deviation_le line 917
  77. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.inheritedMask_rejection_le line 947
  78. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.finite_inheritedMask_rejection_le line 971
  79. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.pushforward_sum_rejection_le line 984
  80. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalTwoHalfCount line 1026
  81. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_totalTwoHalfCount_test line 1030
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_totalTwoHalfCounts_test line 1042
  83. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.twoHalf_pushforward_sum_rejection_le line 1059
  84. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.twoHalf_inheritedMask_rejection_le line 1074
  85. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedTwoHalfCount line 1086
  86. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedTwoHalfMask_rejection_le line 1091
  87. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.finite_selectedTwoHalfMask_rejection_le line 1114
  88. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.inverse_linear_mask_constant line 1131
  89. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.finite_selectedTwoHalfMask_inverse_linear line 1142
  90. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.statisticPositions_card line 1168
  91. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.average_bad_shift_eq_orbit_fraction line 1184
  92. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.classWeight line 1220
  93. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.classDensity line 1223
  94. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.classProductMixture line 1226
  95. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.classWeight_nonneg line 1231
  96. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.sum_classWeight line 1235
  97. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.classDensity_nonneg line 1242
  98. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.classDensity_le_one line 1246
  99. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingMean_normalized_eq line 1254
  100. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingMean_prescribed_error line 1269
  101. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingMean_inherited_margin line 1288
  102. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.inheritedMask_rejection_of_windows_le line 1306
  103. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.twoHalf_inheritedMask_rejection_of_windows_le line 1322
  104. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedTwoHalfMask_rejection_of_windows_le line 1338
  105. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.classDensity_statisticPositions line 1371
  106. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.totalMatchingMean_statistic_eq line 1378
  107. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.twoHalf_statistic_rejection_of_typeWindows_le line 1390
  108. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.selectedTwoHalf_statistic_rejection_of_completeWindows_le line 1421