OAI/Probability/ThorpRouting/Adaptive/RotationMeeting.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Adaptive.Thorp.rotationMeeting line 14
  2. lemma OAI.ThorpNine.Adaptive.Thorp.card_cycleFiber line 22
  3. lemma OAI.ThorpNine.Adaptive.Thorp.terminal_mean line 27
  4. lemma OAI.ThorpNine.Adaptive.Thorp.slotWeight_antitone line 41
  5. lemma OAI.ThorpNine.Adaptive.Thorp.rotationMeeting_mean line 50
  6. lemma OAI.ThorpNine.Adaptive.Thorp.pathWeight_sum line 83
  7. lemma OAI.ThorpNine.Adaptive.Thorp.withinWeight_sum_bound line 100
  8. def OAI.ThorpNine.Adaptive.Thorp.rotationCharge line 122
  9. lemma OAI.ThorpNine.Adaptive.Thorp.rotationCharge_mean_bound line 126
  10. lemma OAI.ThorpNine.Adaptive.Thorp.rotation_exp_bound line 144
  11. def OAI.ThorpNine.Adaptive.Thorp.orbitSet line 166
  12. lemma OAI.ThorpNine.Adaptive.Thorp.mem_orbitSet line 169
  13. lemma OAI.ThorpNine.Adaptive.Thorp.orbitSet_nonempty line 174
  14. lemma OAI.ThorpNine.Adaptive.Thorp.orbitSet_eq line 177
  15. lemma OAI.ThorpNine.Adaptive.Thorp.orbitSet_apply line 183
  16. lemma OAI.ThorpNine.Adaptive.Thorp.orbitSet_eq_or_disjoint line 187
  17. lemma OAI.ThorpNine.Adaptive.Thorp.perm_minimalPeriod_pos line 198
  18. lemma OAI.ThorpNine.Adaptive.Thorp.orbitSet_card line 202
  19. def OAI.ThorpNine.Adaptive.Thorp.walkSet line 221
  20. lemma OAI.ThorpNine.Adaptive.Thorp.mem_walkSet line 225
  21. lemma OAI.ThorpNine.Adaptive.Thorp.walkSet_zero line 230
  22. lemma OAI.ThorpNine.Adaptive.Thorp.walkSet_succ_last line 234
  23. lemma OAI.ThorpNine.Adaptive.Thorp.walkSet_succ_first line 239
  24. lemma OAI.ThorpNine.Adaptive.Thorp.not_mem_short_walk line 253
  25. lemma OAI.ThorpNine.Adaptive.Thorp.walkSet_period line 262
  26. lemma OAI.ThorpNine.Adaptive.Thorp.walkSet_card line 276
  27. lemma OAI.ThorpNine.Adaptive.Thorp.walkSet_subset_orbit line 285
  28. def OAI.ThorpNine.Adaptive.Thorp.cycleTrace line 292
  29. lemma OAI.ThorpNine.Adaptive.Thorp.cycleTrace_walk line 297
  30. lemma OAI.ThorpNine.Adaptive.Thorp.cycleTrace_orbit line 331
  31. def OAI.ThorpNine.Adaptive.Thorp.exposedPaths line 353
  32. lemma OAI.ThorpNine.Adaptive.Thorp.exposedPaths_empty line 357
  33. lemma OAI.ThorpNine.Adaptive.Thorp.exposedPaths_insert line 361
  34. def OAI.ThorpNine.Adaptive.Thorp.terminalCharge line 366
  35. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.followPath_stale_charge line 371
  36. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.seekCycle_semantics line 383
  37. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.seekCycle_orbit line 413
  38. lemma OAI.ThorpNine.Adaptive.Thorp.mem_exposedPaths line 428
  39. lemma OAI.ThorpNine.Adaptive.Thorp.terminalCharge_sum line 440
  40. def OAI.ThorpNine.Adaptive.Thorp.priorPaths line 462
  41. lemma OAI.ThorpNine.Adaptive.Thorp.mem_priorPaths line 465
  42. lemma OAI.ThorpNine.Adaptive.Thorp.terminalCharge_prior_sum line 470
  43. lemma OAI.ThorpNine.Adaptive.Thorp.rotationMeeting_eq_slot_sum line 487
  44. lemma OAI.ThorpNine.Adaptive.Thorp.rotationCharge_eq_terminal_sum line 539
  45. lemma OAI.ThorpNine.Adaptive.Thorp.priorPaths_zero line 546
  46. lemma OAI.ThorpNine.Adaptive.Thorp.priorPaths_succ line 551
  47. lemma OAI.ThorpNine.Adaptive.Thorp.priorPaths_disjoint line 566
  48. lemma OAI.ThorpNine.Adaptive.Thorp.QueryTree.seekCycles_owned line 578
  49. def OAI.ThorpNine.Adaptive.Thorp.ValidCycleSlots line 627
  50. abbrev OAI.ThorpNine.Adaptive.Thorp.CycleSlots line 633
  51. instance OAI.ThorpNine.Adaptive.Thorp.(instance at line 636) line 636
  52. lemma OAI.ThorpNine.Adaptive.Thorp.CycleSlots.terminal_nonempty line 639
  53. lemma OAI.ThorpNine.Adaptive.Thorp.owner_ext line 645
  54. abbrev OAI.ThorpNine.Adaptive.Thorp.RootedSlots line 657
  55. def OAI.ThorpNine.Adaptive.Thorp.rootedStart line 660
  56. lemma OAI.ThorpNine.Adaptive.Thorp.rootedStart_injective line 666
  57. lemma OAI.ThorpNine.Adaptive.Thorp.sum_comp_injective_le line 679
  58. lemma OAI.ThorpNine.Adaptive.Thorp.rooted_weight_sum_le line 687
  59. def OAI.ThorpNine.Adaptive.Thorp.rotationLower line 713
  60. def OAI.ThorpNine.Adaptive.Thorp.collectionWeight line 716
  61. lemma OAI.ThorpNine.Adaptive.Thorp.collectionWeight_pos line 719
  62. lemma OAI.ThorpNine.Adaptive.Thorp.collection_rotation_lower line 723
  63. lemma OAI.ThorpNine.Adaptive.Thorp.cycleSlots_weighted_moment line 751
  64. lemma OAI.ThorpNine.Adaptive.Thorp.cycleSlots_moment line 784
  65. lemma OAI.ThorpNine.Adaptive.Thorp.collectionWeight_eq_sqrt line 790
  66. lemma OAI.ThorpNine.Adaptive.Thorp.butterfly_cycleSlots_moment line 815
  67. abbrev OAI.ThorpNine.Adaptive.Thorp.SelectedCycle line 829
  68. instance OAI.ThorpNine.Adaptive.Thorp.(instance at line 832) line 832
  69. lemma OAI.ThorpNine.Adaptive.Thorp.SelectedCycle.nonempty line 835
  70. lemma OAI.ThorpNine.Adaptive.Thorp.SelectedCycle.orbit_eq line 841
  71. lemma OAI.ThorpNine.Adaptive.Thorp.SelectedCycle.eq_of_mem line 847
  72. abbrev OAI.ThorpNine.Adaptive.Thorp.SlotAssignment line 852
  73. instance OAI.ThorpNine.Adaptive.Thorp.(instance at line 855) line 855
  74. def OAI.ThorpNine.Adaptive.Thorp.slotsToAssignment line 858
  75. def OAI.ThorpNine.Adaptive.Thorp.assignmentOwner line 872