OAI/Analysis/BoundedHochschild/WalkSelection.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Concatenation estimates and finite and countable random-walk selection.

  1. def OAI.HochschildWalk.flattenRows line 25
  2. lemma OAI.HochschildWalk.word_flattenRows line 29
  3. def OAI.HochschildWalk.orientRow line 49
  4. lemma OAI.HochschildWalk.word_orientRow line 53
  5. def OAI.HochschildWalk.blockIndex line 60
  6. lemma OAI.HochschildWalk.blockIndex_injective line 64
  7. lemma OAI.HochschildWalk.concatenated_preserving line 77
  8. lemma OAI.HochschildWalk.flattenRows_prefix line 89
  9. theorem OAI.HochschildWalk.concatenated_cauchy_bound line 103
  10. lemma OAI.HochschildWalk.rows_preserving line 136
  11. lemma OAI.HochschildWalk.rows_event_mass line 147
  12. theorem OAI.HochschildProbability.finite_requirements_eventually line 163
  13. theorem OAI.HochschildProbability.select_finite_stages line 185
  14. def OAI.HochschildWalk.evalList line 212
  15. lemma OAI.HochschildWalk.evalList_ofFn line 216
  16. lemma OAI.HochschildWalk.list_cauchy_bound line 221
  17. theorem OAI.HochschildWalk.finite_walk_selection line 251
  18. theorem OAI.HochschildFiniteTests.finite_alphabet line 321
  19. lemma OAI.HochschildFiniteTests.map_back_word line 329
  20. lemma OAI.HochschildFiniteTests.map_ne_one line 342
  21. lemma OAI.HochschildFiniteTests.map_nodup line 349
  22. lemma OAI.HochschildFiniteTests.lift_map line 360
  23. theorem OAI.HochschildFiniteTests.countable_constraints line 369
  24. def OAI.HochschildWalk.FreeMomentsInProbability line 403
  25. lemma OAI.HochschildWalk.evalList_map line 409
  26. theorem OAI.HochschildWalk.finite_countable_selection line 415
  27. theorem OAI.HochschildWalk.infinite_walk_selection line 465