OAI/Analysis/BoundedHochschild/FreeWords.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Reduced free words, cancellation fibers and repeated-letter bounds.

  1. def OAI.HochschildFreeWords.charge line 13
  2. theorem OAI.HochschildFreeWords.charge_true line 14
  3. theorem OAI.HochschildFreeWords.charge_false line 15
  4. theorem OAI.HochschildFreeWords.charge_not line 16
  5. def OAI.HochschildFreeWords.total line 18
  6. theorem OAI.HochschildFreeWords.total_nil line 19
  7. theorem OAI.HochschildFreeWords.total_cons line 20
  8. theorem OAI.HochschildFreeWords.total_append line 22
  9. theorem OAI.HochschildFreeWords.total_reverse line 24
  10. def OAI.HochschildFreeWords.Above line 27
  11. theorem OAI.HochschildFreeWords.above_nil line 30
  12. theorem OAI.HochschildFreeWords.above_cons line 31
  13. lemma OAI.HochschildFreeWords.above_start line 33
  14. lemma OAI.HochschildFreeWords.above_mono line 37
  15. lemma OAI.HochschildFreeWords.above_append line 42
  16. lemma OAI.HochschildFreeWords.above_cancel line 53
  17. lemma OAI.HochschildFreeWords.total_step line 61
  18. lemma OAI.HochschildFreeWords.above_step line 68
  19. lemma OAI.HochschildFreeWords.above_reverse_step line 72
  20. lemma OAI.HochschildFreeWords.above_red line 80
  21. lemma OAI.HochschildFreeWords.above_reverse_red line 85
  22. lemma OAI.HochschildFreeWords.total_red line 90
  23. lemma OAI.HochschildFreeWords.above_head line 94
  24. inductive OAI.HochschildFreeWords.OddBlock line 105
  25. lemma OAI.HochschildFreeWords.OddBlock.total line 109
  26. lemma OAI.HochschildFreeWords.OddBlock.above line 113
  27. lemma OAI.HochschildFreeWords.OddBlock.above_reverse line 117
  28. lemma OAI.HochschildFreeWords.blocks_total line 125
  29. lemma OAI.HochschildFreeWords.blocks_above line 133
  30. theorem OAI.HochschildFreeWords.ordered_blocks_reduced line 147
  31. def OAI.HochschildFreeWords.insertPair line 169
  32. theorem OAI.HochschildFreeWords.length_insertPair line 171
  33. lemma OAI.HochschildFreeWords.insertPair_append line 176
  34. def OAI.HochschildFreeWords.expansions line 182
  35. lemma OAI.HochschildFreeWords.mem_expansions_length line 186
  36. lemma OAI.HochschildFreeWords.expansions_insert line 197
  37. lemma OAI.HochschildFreeWords.red_mem_expansions line 202
  38. lemma OAI.HochschildFreeWords.mem_expansions_of_reduce line 214
  39. lemma OAI.HochschildFreeWords.card_expansions_succ line 219
  40. theorem OAI.HochschildFreeWords.card_expansions_le line 240
  41. theorem OAI.HochschildFreeWords.reduction_fiber_bound line 256
  42. theorem OAI.HochschildFreeWords.normalized_reduction_fiber_bound line 276
  43. def OAI.HochschildFreeWords.allWords line 310
  44. lemma OAI.HochschildFreeWords.cons_pair_injective line 315
  45. lemma OAI.HochschildFreeWords.mem_allWords line 320
  46. lemma OAI.HochschildFreeWords.card_allWords line 328
  47. def OAI.HochschildFreeWords.badWords line 335
  48. lemma OAI.HochschildFreeWords.mem_badWords line 337
  49. lemma OAI.HochschildFreeWords.card_badWords_one line 340
  50. lemma OAI.HochschildFreeWords.card_badWords_succ line 347
  51. theorem OAI.HochschildFreeWords.card_badWords_le line 386