OAI/Algebra/GroupRing/BalancedPieces.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.BalancedPieces.count line 11
  2. def OAI.TorsionFreeZeroDivisors.BalancedPieces.length line 12
  3. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.sum_length line 13
  4. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.length_pos line 24
  5. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.count_bounds line 28
  6. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.count_le line 42
  7. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.quotient_bounds line 46
  8. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.length_bounds line 69
  9. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.count_charge line 81
  10. def OAI.TorsionFreeZeroDivisors.BalancedPieces.number line 87
  11. def OAI.TorsionFreeZeroDivisors.BalancedPieces.sizes line 88
  12. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.number_pos line 90
  13. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.sizes_sum line 96
  14. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.sizes_pos line 102
  15. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.sizes_upper line 109
  16. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.sizes_lower_long line 118
  17. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.number_charge line 127
  18. lemma OAI.TorsionFreeZeroDivisors.BalancedPieces.sizes_lower line 133
  19. def OAI.TorsionFreeZeroDivisors.ConsecutivePieces.index line 144
  20. def OAI.TorsionFreeZeroDivisors.ConsecutivePieces.offset line 145
  21. lemma OAI.TorsionFreeZeroDivisors.ConsecutivePieces.index_val line 146
  22. def OAI.TorsionFreeZeroDivisors.ConsecutivePieces.segment line 148
  23. lemma OAI.TorsionFreeZeroDivisors.ConsecutivePieces.length_segment line 149
  24. lemma OAI.TorsionFreeZeroDivisors.ConsecutivePieces.segment_get line 150
  25. lemma OAI.TorsionFreeZeroDivisors.ConsecutivePieces.segment_nonempty line 153
  26. lemma OAI.TorsionFreeZeroDivisors.ConsecutivePieces.successor_index line 158
  27. lemma OAI.TorsionFreeZeroDivisors.ConsecutivePieces.segment_chain line 163
  28. lemma OAI.TorsionFreeZeroDivisors.ConsecutivePieces.total_length line 174
  29. lemma OAI.TorsionFreeZeroDivisors.ConsecutivePieces.occurrence_unique line 177

    Source documentation

    Every original occurrence is retained exactly once, at its actual index.

    lemma occurrence_unique (j : Fin l.length) :
    ∃! p : (i : Fin m) × Fin (n i),index l n hs p=j := (index l n hs).bijective.existsUnique j
…

    Mentions: OAI.TorsionFreeZeroDivisors.ConsecutivePieces.index

  30. abbrev OAI.TorsionFreeZeroDivisors.BalancedWords.Piece line 183
  31. def OAI.TorsionFreeZeroDivisors.BalancedWords.old line 184
  32. def OAI.TorsionFreeZeroDivisors.BalancedWords.segment line 185
  33. lemma OAI.TorsionFreeZeroDivisors.BalancedWords.segment_length line 188
  34. lemma OAI.TorsionFreeZeroDivisors.BalancedWords.old_pos line 191
  35. lemma OAI.TorsionFreeZeroDivisors.BalancedWords.segment_nonempty line 193
  36. lemma OAI.TorsionFreeZeroDivisors.BalancedWords.segment_chain line 197
  37. lemma OAI.TorsionFreeZeroDivisors.BalancedWords.old_le line 199
  38. lemma OAI.TorsionFreeZeroDivisors.BalancedWords.intact line 201
  39. lemma OAI.TorsionFreeZeroDivisors.BalancedWords.old_sum line 223
  40. lemma OAI.TorsionFreeZeroDivisors.BalancedWords.closure_charge line 231

    Source documentation

    Quantitative closing, before identifying the added positions as fixed. Only genuinely split words get closure terms.

    lemma closure_charge (tail : Piece w cap → List A) (tailCap : ℕ) (hcap : 6≤cap)
    (hshort : ∀ p,(w p.1).length≤cap → tail p=[])
    (htail : ∀ p,(tail p).length≤tailCap) :
    cap*(∑p,(tail p).length)≤3*tailCap*(∑t,(w t).length) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BalancedWords.Piece

  41. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.endpoint_cons' line 255
  42. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath.exists_walk line 261
  43. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath.length_ge line 277
  44. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.of_cyclic line 287
  45. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.Piece line 306
  46. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.seg line 307
  47. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.seg_ne line 308
  48. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.start line 310
  49. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.segment_path line 311
  50. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.D line 321
  51. def OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.chosenTail line 323
  52. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.chosenTail_spec line 325
  53. def OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.tail line 334
  54. def OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.word line 336
  55. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.tail_short line 337
  56. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.tail_bound line 338
  57. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.word_short line 343
  58. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.nonempty line 346
  59. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.chain line 349
  60. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.cyclic_of_long line 355
  61. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.original_girth line 361
  62. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.old_le_word line 366
  63. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.word_bound line 369
  64. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.total_added line 374