OAI/GroupTheory/PeriodicGroups/Algebra/HierarchyGrowth.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.HierarchyGrowth.height line 11
  2. def OAI.SourceBurnside.HierarchyGrowth.dimension line 13
  3. def OAI.SourceBurnside.HierarchyGrowth.exponent line 17
  4. lemma OAI.SourceBurnside.HierarchyGrowth.height_succ line 20
  5. lemma OAI.SourceBurnside.HierarchyGrowth.exponent_succ line 23
  6. lemma OAI.SourceBurnside.HierarchyGrowth.dimension_bound line 27
  7. lemma OAI.SourceBurnside.HierarchyGrowth.geometric_identity line 41
  8. lemma OAI.SourceBurnside.HierarchyGrowth.source_choice line 50
  9. theorem OAI.SourceBurnside.HierarchyGrowth.stopping_index line 57
  10. def OAI.SourceBurnside.WeightedTests.product line 102
  11. def OAI.SourceBurnside.WeightedTests.length line 105
  12. lemma OAI.SourceBurnside.WeightedTests.length_ge line 108
  13. lemma OAI.SourceBurnside.WeightedTests.sum_product_eq_pow line 114
  14. def OAI.SourceBurnside.WeightedTests.lengthPolynomial line 126
  15. lemma OAI.SourceBurnside.WeightedTests.coefficient_lengthPolynomial line 130
  16. theorem OAI.SourceBurnside.WeightedTests.nilpotent_of_eventually_zero_lengthPolynomial line 147
  17. def OAI.SourceBurnside.Cuts.parse line 179
  18. def OAI.SourceBurnside.Cuts.NoCut line 185
  19. def OAI.SourceBurnside.Cuts.Interval line 187
  20. lemma OAI.SourceBurnside.Cuts.parse_join line 190
  21. lemma OAI.SourceBurnside.Cuts.parse_prefix line 199
  22. lemma OAI.SourceBurnside.Cuts.parse_intervals line 211
  23. lemma OAI.SourceBurnside.Cuts.parse_noCut_append line 224
  24. lemma OAI.SourceBurnside.Cuts.parse_interval_append line 233
  25. lemma OAI.SourceBurnside.Cuts.parse_intervals_flatten line 238
  26. theorem OAI.SourceBurnside.Cuts.parse_language line 247
  27. theorem OAI.SourceBurnside.Cuts.language_injective line 260
  28. def OAI.SourceBurnside.FiniteTable.Token line 279
  29. def OAI.SourceBurnside.FiniteTable.fragmentBound line 281
  30. lemma OAI.SourceBurnside.FiniteTable.token_normal_form line 282
  31. lemma OAI.SourceBurnside.FiniteTable.token_length_le line 287
  32. lemma OAI.SourceBurnside.FiniteTable.finite_tokens line 290
  33. lemma OAI.SourceBurnside.FiniteTable.flatten_member_infix line 292
  34. lemma OAI.SourceBurnside.FiniteTable.token_of_adjacent line 296
  35. lemma OAI.SourceBurnside.FiniteTable.tokens_of_flatten line 300
  36. theorem OAI.SourceBurnside.FiniteTable.Survives.token_decomposition line 320
  37. lemma OAI.SourceBurnside.FiniteTable.Survives.palette_rank_mono line 363
  38. lemma OAI.SourceBurnside.FiniteTable.Survives.long_equal_rank line 372
  39. lemma OAI.SourceBurnside.FiniteTable.Survives.equal_rank_eligible line 427
  40. theorem OAI.SourceBurnside.FiniteTable.Survives.palette_long_eligible line 459
  41. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.palette_card_le line 469
  42. lemma OAI.SourceBurnside.FiniteTable.token_contains_block line 487
  43. lemma OAI.SourceBurnside.FiniteTable.token_long_eligible line 501
  44. theorem OAI.SourceBurnside.FiniteTable.Survives.long_eligible line 509
  45. lemma OAI.SourceBurnside.FiniteTable.Codec.Survives.infix line 526
  46. lemma OAI.SourceBurnside.FiniteTable.Codec.Survives.has_encoding line 531
  47. def OAI.SourceBurnside.FiniteTable.Codec.rawCut line 553
  48. lemma OAI.SourceBurnside.FiniteTable.Codec.rawCut_encode line 554
  49. def OAI.SourceBurnside.FiniteTable.Codec.noncolor line 557
  50. def OAI.SourceBurnside.FiniteTable.Codec.fields line 558
  51. def OAI.SourceBurnside.FiniteTable.Codec.eligibleFields line 559
  52. lemma OAI.SourceBurnside.FiniteTable.Codec.fields_encode line 560
  53. lemma OAI.SourceBurnside.FiniteTable.Codec.erased_palette line 562
  54. lemma OAI.SourceBurnside.FiniteTable.Codec.erased_headfree line 565
  55. lemma OAI.SourceBurnside.FiniteTable.Codec.Survives.long_uniform line 566
  56. def OAI.SourceBurnside.FiniteTable.Codec.rawToken line 582
  57. lemma OAI.SourceBurnside.FiniteTable.Codec.finite_rawTokens line 584
  58. lemma OAI.SourceBurnside.FiniteTable.Codec.rawToken_interval line 589
  59. lemma OAI.SourceBurnside.FiniteTable.Codec.rawToken_normalize line 597
  60. theorem OAI.SourceBurnside.FiniteTable.Codec.Survives.raw_token_decomposition line 607