OAI/Analysis/BoundedHochschild/CatalanWords.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Binary-tree enumeration of return words and normalized Catalan moments.

  1. def OAI.HochschildCatalanWords.word line 17
  2. lemma OAI.HochschildCatalanWords.length_word line 21
  3. def OAI.HochschildCatalanWords.unorientedReduce line 27
  4. def OAI.HochschildCatalanWords.signed line 34
  5. lemma OAI.HochschildCatalanWords.signed_eq_nil line 38
  6. lemma OAI.HochschildCatalanWords.reduce_signed line 41
  7. def OAI.HochschildCatalanWords.render line 55
  8. def OAI.HochschildCatalanWords.parse line 59
  9. lemma OAI.HochschildCatalanWords.render_parse line 65
  10. lemma OAI.HochschildCatalanWords.unmatched_parse line 83
  11. theorem OAI.HochschildCatalanWords.exists_tree_of_reduce_signed_eq_nil line 98
  12. lemma OAI.HochschildCatalanWords.signed_append_even line 108
  13. lemma OAI.HochschildCatalanWords.signed_word_node line 117
  14. lemma OAI.HochschildCatalanWords.reduce_signed_word line 123
  15. def OAI.HochschildCatalanWords.labels line 136
  16. lemma OAI.HochschildCatalanWords.length_labels line 140
  17. lemma OAI.HochschildCatalanWords.mem_word_iff line 145
  18. lemma OAI.HochschildCatalanWords.delimiter_split line 150
  19. theorem OAI.HochschildCatalanWords.word_injective_on_nodup line 176
  20. def OAI.HochschildCatalanWords.shape line 199
  21. lemma OAI.HochschildCatalanWords.numNodes_shape line 201
  22. def OAI.HochschildCatalanWords.decorate line 207
  23. lemma OAI.HochschildCatalanWords.decorate_spec line 213
  24. lemma OAI.HochschildCatalanWords.decorate_shape_labels line 232
  25. abbrev OAI.HochschildCatalanWords.Shapes line 240
  26. lemma OAI.HochschildCatalanWords.card_shapes line 242
  27. lemma OAI.HochschildCatalanWords.nodes_shape line 245
  28. def OAI.HochschildCatalanWords.listFunction line 248
  29. lemma OAI.HochschildCatalanWords.ofFn_listFunction line 251
  30. abbrev OAI.HochschildCatalanWords.ReturnWords line 256
  31. def OAI.HochschildCatalanWords.treeFrom line 259
  32. lemma OAI.HochschildCatalanWords.shape_treeFrom line 262
  33. lemma OAI.HochschildCatalanWords.labels_treeFrom line 266
  34. lemma OAI.HochschildCatalanWords.nodes_treeFrom line 270
  35. def OAI.HochschildCatalanWords.fromTree line 276
  36. lemma OAI.HochschildCatalanWords.ofFn_fromTree line 280
  37. lemma OAI.HochschildCatalanWords.fromTree_surjective line 284
  38. def OAI.HochschildCatalanWords.fromDistinctTree line 299
  39. lemma OAI.HochschildCatalanWords.fromDistinctTree_injective line 302
  40. theorem OAI.HochschildCatalanWords.returnWord_count_bounds line 322
  41. theorem OAI.HochschildCatalanWords.normalized_returnWord_count_tendsto line 334
  42. def OAI.HochschildCatalanMoments.signedSum line 365
  43. lemma OAI.HochschildCatalanMoments.signedSum_succ line 368
  44. lemma OAI.HochschildCatalanMoments.signedSum_zero line 382
  45. lemma OAI.HochschildCatalanMoments.signedSum_even line 385
  46. lemma OAI.HochschildCatalanMoments.sum_star line 401
  47. lemma OAI.HochschildCatalanMoments.sum_pow_expansion line 408
  48. lemma OAI.HochschildCatalanMoments.trace_word line 418
  49. lemma OAI.HochschildCatalanMoments.trace_sum_pow line 429
  50. def OAI.HochschildCatalanMoments.positiveSum line 437
  51. lemma OAI.HochschildCatalanMoments.trace_positiveSum_pow line 441
  52. lemma OAI.HochschildCatalanMoments.re_trace_positiveSum_pow line 448
  53. theorem OAI.HochschildCatalanMoments.normalized_moments_tendsto line 457