OAI/Analysis/FreeGroupFactor/RankTwoCounting.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.RankTwo.top_power_dominates line 19
  2. theorem OAI.FreeGroupFactorMain.RankTwo.power_sum_ne_zero line 27
  3. def OAI.FreeGroupFactorMain.RankTwo.bExponentHom line 99
  4. def OAI.FreeGroupFactorMain.RankTwo.bExponent line 102
  5. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_one line 104
  6. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_mul line 105
  7. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_inv line 107
  8. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_a line 109
  9. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_b line 111
  10. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_piece line 113
  11. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_segment line 116
  12. def OAI.FreeGroupFactorMain.RankTwo.boolSign line 124
  13. theorem OAI.FreeGroupFactorMain.RankTwo.boolSign_true line 126
  14. theorem OAI.FreeGroupFactorMain.RankTwo.boolSign_false line 127
  15. theorem OAI.FreeGroupFactorMain.RankTwo.boolSign_not line 128
  16. theorem OAI.FreeGroupFactorMain.RankTwo.abs_boolSign line 129
  17. def OAI.FreeGroupFactorMain.RankTwo.labelCoefficient line 131
  18. theorem OAI.FreeGroupFactorMain.RankTwo.labelCoefficient_abs_le line 135
  19. theorem OAI.FreeGroupFactorMain.RankTwo.labelCoefficient_sum_mul line 145
  20. theorem OAI.FreeGroupFactorMain.RankTwo.labelCoefficient_eq_zero line 155
  21. def OAI.FreeGroupFactorMain.RankTwo.AdjacentValues line 176
  22. def OAI.FreeGroupFactorMain.RankTwo.Covers line 179
  23. theorem OAI.FreeGroupFactorMain.RankTwo.covers_iff line 181
  24. def OAI.FreeGroupFactorMain.RankTwo.adjacentPairs line 191
  25. theorem OAI.FreeGroupFactorMain.RankTwo.card_adjacentPairs_le line 194
  26. def OAI.FreeGroupFactorMain.RankTwo.adjacentFunctions line 219
  27. theorem OAI.FreeGroupFactorMain.RankTwo.adjacentFunctions_eq line 223
  28. theorem OAI.FreeGroupFactorMain.RankTwo.card_adjacentFunctions_le line 230
  29. def OAI.FreeGroupFactorMain.RankTwo.coveredPairs line 244
  30. def OAI.FreeGroupFactorMain.RankTwo.badCoveredPairs line 248
  31. theorem OAI.FreeGroupFactorMain.RankTwo.coveredPairs_param line 252
  32. theorem OAI.FreeGroupFactorMain.RankTwo.card_coveredPairs_le line 269
  33. theorem OAI.FreeGroupFactorMain.RankTwo.badCoveredPairs_param line 276
  34. theorem OAI.FreeGroupFactorMain.RankTwo.card_badCoveredPairs_le line 296
  35. def OAI.FreeGroupFactorMain.RankTwo.coloredEncode line 308
  36. theorem OAI.FreeGroupFactorMain.RankTwo.coloredEncode_injective line 313
  37. def OAI.FreeGroupFactorMain.RankTwo.ColoredCovers line 326
  38. def OAI.FreeGroupFactorMain.RankTwo.ColoredAdjacent line 329
  39. theorem OAI.FreeGroupFactorMain.RankTwo.coloredEncode_covers line 332
  40. theorem OAI.FreeGroupFactorMain.RankTwo.coloredEncode_adjacent line 341
  41. theorem OAI.FreeGroupFactorMain.RankTwo.card_coloredCovered_le line 349
  42. theorem OAI.FreeGroupFactorMain.RankTwo.card_coloredBad_le line 363
  43. def OAI.FreeGroupFactorMain.RankTwo.prefixHom line 382
  44. def OAI.FreeGroupFactorMain.RankTwo.patternWord line 385
  45. def OAI.FreeGroupFactorMain.RankTwo.pairColors line 388
  46. def OAI.FreeGroupFactorMain.RankTwo.pairLabels line 391
  47. theorem OAI.FreeGroupFactorMain.RankTwo.pairLabels_injective line 394
  48. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_lift_mk line 401
  49. theorem OAI.FreeGroupFactorMain.RankTwo.bExponent_pattern line 411
  50. theorem OAI.FreeGroupFactorMain.RankTwo.covers_of_balanced line 419
  51. theorem OAI.FreeGroupFactorMain.RankTwo.collision_covers line 441
  52. theorem OAI.FreeGroupFactorMain.RankTwo.separated_of_covers line 457
  53. theorem OAI.FreeGroupFactorMain.RankTwo.collision_free_of_separated line 469
  54. theorem OAI.FreeGroupFactorMain.RankTwo.collision_bad_adjacent line 496
  55. theorem OAI.FreeGroupFactorMain.RankTwo.card_patternCollisions_le line 508
  56. theorem OAI.FreeGroupFactorMain.RankTwo.card_patternBadCollisions_le line 525
  57. theorem OAI.FreeGroupFactorMain.RankTwo.card_patternCollisions_le_free_add line 543
  58. def OAI.FreeGroupFactorMain.RankTwo.alternating line 568
  59. theorem OAI.FreeGroupFactorMain.RankTwo.alternating_zero line 572
  60. theorem OAI.FreeGroupFactorMain.RankTwo.alternating_succ line 573
  61. theorem OAI.FreeGroupFactorMain.RankTwo.signed_ofFn line 576
  62. theorem OAI.FreeGroupFactorMain.RankTwo.vertex_ofFn line 584
  63. def OAI.FreeGroupFactorMain.RankTwo.positiveCount line 589
  64. theorem OAI.FreeGroupFactorMain.RankTwo.positiveCount_zero line 591
  65. theorem OAI.FreeGroupFactorMain.RankTwo.positiveCount_succ line 592
  66. theorem OAI.FreeGroupFactorMain.RankTwo.positiveCount_two line 597
  67. theorem OAI.FreeGroupFactorMain.RankTwo.positiveCount_even line 601
  68. theorem OAI.FreeGroupFactorMain.RankTwo.positiveCount_odd line 606
  69. theorem OAI.FreeGroupFactorMain.RankTwo.card_alternating_pos line 610
  70. theorem OAI.FreeGroupFactorMain.RankTwo.card_alternating_neg line 616
  71. theorem OAI.FreeGroupFactorMain.RankTwo.alternating_charge line 622
  72. theorem OAI.FreeGroupFactorMain.RankTwo.card_pairColors_pos line 633
  73. theorem OAI.FreeGroupFactorMain.RankTwo.card_pairColors_neg line 643
  74. def OAI.FreeGroupFactorMain.coefficientPair line 655
  75. theorem OAI.FreeGroupFactorMain.coefficientPair_self line 657
  76. theorem OAI.FreeGroupFactorMain.coefficientPair_zero_left line 664
  77. theorem OAI.FreeGroupFactorMain.coefficientPair_single_left line 667
  78. theorem OAI.FreeGroupFactorMain.coefficientPair_add_left line 670
  79. theorem OAI.FreeGroupFactorMain.coefficientPair_sum_left line 674
  80. theorem OAI.FreeGroupFactorMain.coefficientPair_zero_right line 681
  81. theorem OAI.FreeGroupFactorMain.coefficientPair_add_right line 684
  82. theorem OAI.FreeGroupFactorMain.coefficientPair_single_right line 688
  83. theorem OAI.FreeGroupFactorMain.coefficientPair_sum_right line 694
  84. theorem OAI.FreeGroupFactorMain.coefficientPair_smul_left line 701
  85. theorem OAI.FreeGroupFactorMain.coefficientPair_smul_right line 707
  86. theorem OAI.FreeGroupFactorMain.coefficientPair_single_sums line 712
  87. theorem OAI.FreeGroupFactorMain.coefficientPair_shells line 728