OAI/Combinatorics/TreeEdit/RandomCircle.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TreeEdit.TorusTree.representative_toAddCircle line 10
  2. lemma OAI.TreeEdit.TorusTree.bin_grid line 19
  3. lemma OAI.TreeEdit.TorusTree.bin_grid_step line 33
  4. lemma OAI.TreeEdit.TorusTree.mean_comp_hom line 63
  5. lemma OAI.TreeEdit.TorusTree.mean_translate line 70
  6. def OAI.TreeEdit.TorusTree.mapState line 73
  7. lemma OAI.TreeEdit.TorusTree.mapState_diagonal line 78
  8. def OAI.TreeEdit.TorusTree.sample line 85
  9. def OAI.TreeEdit.TorusTree.child line 88
  10. def OAI.TreeEdit.TorusTree.sampledWord line 91
  11. lemma OAI.TreeEdit.TorusTree.point_grid line 96
  12. lemma OAI.TreeEdit.TorusTree.bin_step_mean line 107
  13. lemma OAI.TreeEdit.TorusTree.mean_eval line 138
  14. def OAI.TreeEdit.TorusTree.cycle line 143
  15. lemma OAI.TreeEdit.TorusTree.sampledWord_succ line 148
  16. lemma OAI.TreeEdit.TorusTree.sampledWord_diagonal_step line 165
  17. lemma OAI.TreeEdit.TorusTree.mean_ed_add line 222
  18. lemma OAI.TreeEdit.TorusTree.mean_ed_nsmul line 230
  19. lemma OAI.TreeEdit.TorusTree.sampledWord_tiny line 242
  20. lemma OAI.TreeEdit.TorusTree.sampledWord_cycle_cost line 267
  21. lemma OAI.TreeEdit.TorusTree.cycle_period line 284
  22. lemma OAI.TreeEdit.TorusTree.sampledWord_child_mean line 302