OAI/Probability/ThorpRouting/HighTail/RotationMeeting.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.HighTail.Thorp.rotationMeeting line 14
  2. lemma OAI.ThorpNine.HighTail.Thorp.card_cycleFiber line 22
  3. lemma OAI.ThorpNine.HighTail.Thorp.terminal_mean line 27
  4. lemma OAI.ThorpNine.HighTail.Thorp.slotWeight_antitone line 41
  5. lemma OAI.ThorpNine.HighTail.Thorp.rotationMeeting_mean line 50
  6. lemma OAI.ThorpNine.HighTail.Thorp.pathWeight_sum line 83
  7. lemma OAI.ThorpNine.HighTail.Thorp.withinWeight_sum_bound line 100
  8. def OAI.ThorpNine.HighTail.Thorp.rotationCharge line 122
  9. lemma OAI.ThorpNine.HighTail.Thorp.rotationCharge_mean_bound line 126
  10. lemma OAI.ThorpNine.HighTail.Thorp.rotation_exp_bound line 144
  11. lemma OAI.ThorpNine.HighTail.Thorp.mem_orbitSet line 166
  12. lemma OAI.ThorpNine.HighTail.Thorp.orbitSet_nonempty line 171
  13. lemma OAI.ThorpNine.HighTail.Thorp.orbitSet_eq line 174
  14. lemma OAI.ThorpNine.HighTail.Thorp.orbitSet_apply line 180
  15. lemma OAI.ThorpNine.HighTail.Thorp.orbitSet_eq_or_disjoint line 184
  16. lemma OAI.ThorpNine.HighTail.Thorp.perm_minimalPeriod_pos line 195
  17. lemma OAI.ThorpNine.HighTail.Thorp.orbitSet_card line 199
  18. def OAI.ThorpNine.HighTail.Thorp.walkSet line 218
  19. lemma OAI.ThorpNine.HighTail.Thorp.mem_walkSet line 222
  20. lemma OAI.ThorpNine.HighTail.Thorp.walkSet_zero line 227
  21. lemma OAI.ThorpNine.HighTail.Thorp.walkSet_succ_last line 231
  22. lemma OAI.ThorpNine.HighTail.Thorp.walkSet_succ_first line 236
  23. lemma OAI.ThorpNine.HighTail.Thorp.not_mem_short_walk line 250
  24. lemma OAI.ThorpNine.HighTail.Thorp.walkSet_period line 259
  25. lemma OAI.ThorpNine.HighTail.Thorp.walkSet_card line 273
  26. lemma OAI.ThorpNine.HighTail.Thorp.walkSet_subset_orbit line 282
  27. def OAI.ThorpNine.HighTail.Thorp.cycleTrace line 289
  28. lemma OAI.ThorpNine.HighTail.Thorp.cycleTrace_walk line 294
  29. lemma OAI.ThorpNine.HighTail.Thorp.cycleTrace_orbit line 328
  30. def OAI.ThorpNine.HighTail.Thorp.exposedPaths line 350
  31. lemma OAI.ThorpNine.HighTail.Thorp.exposedPaths_empty line 354
  32. lemma OAI.ThorpNine.HighTail.Thorp.exposedPaths_insert line 358
  33. def OAI.ThorpNine.HighTail.Thorp.terminalCharge line 363
  34. lemma OAI.ThorpNine.HighTail.Thorp.QueryTree.followPath_stale_charge line 368
  35. lemma OAI.ThorpNine.HighTail.Thorp.QueryTree.seekCycle_semantics line 380
  36. lemma OAI.ThorpNine.HighTail.Thorp.QueryTree.seekCycle_orbit line 410
  37. lemma OAI.ThorpNine.HighTail.Thorp.mem_exposedPaths line 425
  38. lemma OAI.ThorpNine.HighTail.Thorp.terminalCharge_sum line 437
  39. def OAI.ThorpNine.HighTail.Thorp.priorPaths line 459
  40. lemma OAI.ThorpNine.HighTail.Thorp.mem_priorPaths line 462
  41. lemma OAI.ThorpNine.HighTail.Thorp.terminalCharge_prior_sum line 467
  42. lemma OAI.ThorpNine.HighTail.Thorp.rotationMeeting_eq_slot_sum line 484
  43. lemma OAI.ThorpNine.HighTail.Thorp.rotationCharge_eq_terminal_sum line 536
  44. lemma OAI.ThorpNine.HighTail.Thorp.priorPaths_zero line 543
  45. lemma OAI.ThorpNine.HighTail.Thorp.priorPaths_succ line 548
  46. lemma OAI.ThorpNine.HighTail.Thorp.priorPaths_disjoint line 563
  47. lemma OAI.ThorpNine.HighTail.Thorp.QueryTree.seekCycles_owned line 575
  48. def OAI.ThorpNine.HighTail.Thorp.ValidCycleSlots line 624
  49. abbrev OAI.ThorpNine.HighTail.Thorp.CycleSlots line 630
  50. instance OAI.ThorpNine.HighTail.Thorp.(instance at line 633) line 633
  51. lemma OAI.ThorpNine.HighTail.Thorp.CycleSlots.terminal_nonempty line 636
  52. lemma OAI.ThorpNine.HighTail.Thorp.owner_ext line 642
  53. abbrev OAI.ThorpNine.HighTail.Thorp.RootedSlots line 654
  54. def OAI.ThorpNine.HighTail.Thorp.rootedStart line 657
  55. lemma OAI.ThorpNine.HighTail.Thorp.rootedStart_injective line 663
  56. lemma OAI.ThorpNine.HighTail.Thorp.sum_comp_injective_le line 676
  57. lemma OAI.ThorpNine.HighTail.Thorp.rooted_weight_sum_le line 684
  58. def OAI.ThorpNine.HighTail.Thorp.rotationLower line 710
  59. def OAI.ThorpNine.HighTail.Thorp.collectionWeight line 713
  60. lemma OAI.ThorpNine.HighTail.Thorp.collectionWeight_pos line 716
  61. lemma OAI.ThorpNine.HighTail.Thorp.collection_rotation_lower line 720
  62. lemma OAI.ThorpNine.HighTail.Thorp.cycleSlots_weighted_moment line 748
  63. lemma OAI.ThorpNine.HighTail.Thorp.cycleSlots_moment line 781
  64. lemma OAI.ThorpNine.HighTail.Thorp.collectionWeight_eq_sqrt line 787
  65. lemma OAI.ThorpNine.HighTail.Thorp.butterfly_cycleSlots_moment line 812
  66. abbrev OAI.ThorpNine.HighTail.Thorp.SelectedCycle line 826
  67. instance OAI.ThorpNine.HighTail.Thorp.(instance at line 829) line 829
  68. lemma OAI.ThorpNine.HighTail.Thorp.SelectedCycle.nonempty line 832
  69. lemma OAI.ThorpNine.HighTail.Thorp.SelectedCycle.orbit_eq line 838
  70. lemma OAI.ThorpNine.HighTail.Thorp.SelectedCycle.eq_of_mem line 844
  71. abbrev OAI.ThorpNine.HighTail.Thorp.SlotAssignment line 849
  72. instance OAI.ThorpNine.HighTail.Thorp.(instance at line 852) line 852
  73. def OAI.ThorpNine.HighTail.Thorp.slotsToAssignment line 855
  74. def OAI.ThorpNine.HighTail.Thorp.assignmentOwner line 869