OAI/LinearAlgebra/MatrixFields/Histories/GroupOrbitCount.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.support line 18
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.support_card_le line 22
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.support_card_le_exp line 29
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.word_card_eq_exp line 48
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.card_le_exp_of_word_embedding line 61
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.support_card_le_exp_of_word_embeddings line 67
  7. def OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.cw5SupportRate line 81
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.cw5SupportRate_pos line 83
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoverySupport.cw5_support_card_le_exp line 89
  10. abbrev OAI.MatrixAllFields.MatrixMultiplication.HistorySupport.HistoryWords line 120
  11. def OAI.MatrixAllFields.MatrixMultiplication.HistorySupport.totalLength line 123
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySupport.card_historyWords line 131
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySupport.card_historyWords_le_pow line 143
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySupport.card_historyWords_le_exp line 149
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySupport.support_card_le_exp line 160
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.HistorySupport.cw5_support_card_le_exp line 171
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.work_source_amount_pos line 201
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.work_source_population_pos line 209
  19. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.PositiveBranch line 215
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchPopulation_pos_iff line 218
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.positive_branch_minimum line 224
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.positive_joint_class_minimum line 229
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeLengthRate line 237
  24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activePositions line 241
  25. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.(instance at line 245) line 245
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.active_totalLength_cast line 248
  27. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeLengthBudget line 262
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.active_totalLength_le line 265
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.active_cw5_support_bound line 279
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.population_dilation line 317
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.branchPopulation_dilation line 321
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.jointCounts_dilation line 326
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.activeCounts_dilation line 332
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.activeCounts_pos_iff line 337
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.dilation_le_activeCounts line 343
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.two_le_activeCounts line 351
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.totalLength_dilation line 356
  38. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.fixedBaseLength line 363
  39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.supportRate line 368
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.supportRate_pos line 371
  41. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.ActiveRawPairs line 375
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.raw_support_card_le_exp line 379
  43. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.ActiveClass line 392
  44. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selectedBaseCount line 394
  45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selectedBasePopulation line 398
  46. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selectedPositions line 401
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selected_count_dilation line 405
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selectedBaseCount_pos line 410
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selectedBasePopulation_pos line 416
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selected_populationSize line 423
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selected_two_le line 435
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selected_classWeight_formula line 442
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selected_classWeight_eq_one line 452
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.selected_classProductMixture_eq_one line 459
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.work_source_amount_pos line 468
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.work_source_population_pos line 478
  57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.positiveClasses line 483
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_positive line 487
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_baseCount line 491
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_basePopulation_pos line 504
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_nonempty line 510
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_populationSize line 517
  63. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.joinHalves line 548
  64. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.sourcePositionsEquiv line 556
  65. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.incomingWord line 561
  66. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryIncomingMasks.received line 566
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryBranchWeights.stageB_branchPopulation_rat line 592
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryBranchWeights.stageB_branchPopulation_real line 600
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryBranchWeights.stageB_branchWeight_rat line 607
  70. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryBranchWeights.stageB_branchWeight_real line 619
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryBranchWeights.shapeCounts_weighted_sum line 631
  72. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryStageCIncoming.stageCActive line 665
  73. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryStageCIncoming.positionEquiv line 669
  74. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryStageCIncoming.positionEquiv_shape line 679
  75. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryStageCIncoming.positionEquiv_symm_shape line 692
  76. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryStageCIncoming.typeWindow_of_target_side_weights line 703
  77. abbrev OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.PairProfile line 778
  78. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.pairProfile line 781
  79. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.pairProfile_smul line 786
  80. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.completeWordPair_ext line 802
  81. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.pairProfile_eq_iff line 812
  82. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.pairProfile_eq_iff_orbitRel line 834
  83. abbrev OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.PairOrbit line 844
  84. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.pairOrbitProfile line 847
  85. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.pairOrbitProfile_injective line 852
  86. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.card_pairOrbits_le line 864
  87. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.card_pairOrbits_le_common_bound line 879
  88. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.Classes line 915
  89. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.Positions line 917
  90. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.Letters line 921
  91. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.ActualOrbit line 924
  92. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.actualOrbitFintype line 928
  93. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.basePopulationBound line 935
  94. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.orbitDegree line 938
  95. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.card_letters line 941
  96. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.class_card_le line 945
  97. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.card_actualOrbit_le line 959
  98. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.card_actualOrbit_le_polynomial line 971
  99. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.orbitPrefactor line 981
  100. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.orbitPrefactor_pos line 985
  101. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.card_actualOrbit_le_polynomial_real line 990
  102. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.usedOrbits_card_le line 998
  103. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.usedOrbits_card_le_real line 1007
  104. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryOrbitCount.taggedUsedOrbits_card_le_real line 1014
  105. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.GroupClasses line 1053
  106. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.GroupPositions line 1056
  107. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.GroupLetters line 1060
  108. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.GroupOrbit line 1063
  109. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.groupOrbitFintype line 1068
  110. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.groupDegree line 1075
  111. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.card_groupLetters line 1078
  112. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.groupClass_card_le line 1083
  113. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.card_groupOrbit_le line 1089
  114. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.card_groupOrbit_le_polynomial line 1102
  115. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.groupOrbitPrefactor line 1113
  116. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.groupOrbitPrefactor_pos line 1117
  117. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.card_groupOrbit_le_polynomial_real line 1122
  118. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.usedGroupOrbits_card_le_real line 1130
  119. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitCount.taggedUsedGroupOrbits_card_le_real line 1143