OAI/Analysis/TracialCohomology/MarkedWords.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Marked words for bounded Hochschild cohomology.

  1. abbrev OAI.PopaPatching.Mark line 20
  2. abbrev OAI.PopaPatching.Block line 21
  3. def OAI.PopaPatching.oldMark line 22
  4. def OAI.PopaPatching.eraseMark line 23
  5. def OAI.PopaPatching.freshs line 25
  6. def OAI.PopaPatching.markedValue line 29
  7. def OAI.PopaPatching.markedEval line 31
  8. lemma OAI.PopaPatching.erase_old line 34
  9. lemma OAI.PopaPatching.erase_old_list line 35
  10. lemma OAI.PopaPatching.freshs_old line 39
  11. lemma OAI.PopaPatching.freshs_append line 43
  12. lemma OAI.PopaPatching.markedEval_old line 46
  13. lemma OAI.PopaPatching.markedEval_append line 52
  14. def OAI.PopaPatching.variants line 56
  15. lemma OAI.PopaPatching.erase_variant line 62
  16. lemma OAI.PopaPatching.variants_length_le line 81
  17. lemma OAI.PopaPatching.evaluate_add_expansion line 88
  18. def OAI.PopaPatching.splitMarked line 108
  19. def OAI.PopaPatching.flattenBlocks line 114
  20. def OAI.PopaPatching.eraseBlocks line 116
  21. lemma OAI.PopaPatching.splitMarked_spec line 119
  22. lemma OAI.PopaPatching.erase_flatten line 132
  23. lemma OAI.PopaPatching.freshs_flatten line 142
  24. lemma OAI.PopaPatching.markedEval_flatten line 152
  25. def OAI.PopaPatching.appendTail line 161
  26. lemma OAI.PopaPatching.appendTail_spec line 166
  27. lemma OAI.PopaPatching.freshs_nonempty_split line 179
  28. lemma OAI.PopaPatching.degree_rotation_ne_one line 185
  29. lemma OAI.PopaPatching.cyclic_blocks line 191
  30. def OAI.PopaPatching.newVariants line 228
  31. lemma OAI.PopaPatching.variants_eq line 234
  32. lemma OAI.PopaPatching.mem_newVariants line 239
  33. lemma OAI.PopaPatching.newVariants_length_le line 256
  34. lemma OAI.PopaPatching.eraseBlocks_append line 261
  35. lemma OAI.PopaPatching.blocks_length_le line 264
  36. lemma OAI.PopaPatching.segment_length_bound line 272
  37. lemma OAI.PopaPatching.blocks_degree line 282
  38. lemma OAI.PopaPatching.exists_nontrivial_segment line 292
  39. lemma OAI.PopaPatching.evaluate_blocks line 301
  40. lemma OAI.PopaPatching.evaluate_add_new_expansion line 311