OAI/Probability/ThorpRouting/Dense/RotationCharge.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Dense.Thorp.card_cycleFiber line 14
  2. lemma OAI.ThorpNine.Dense.Thorp.terminal_mean line 19
  3. lemma OAI.ThorpNine.Dense.Thorp.slotWeight_antitone line 33
  4. lemma OAI.ThorpNine.Dense.Thorp.rotationMeeting_mean line 42
  5. lemma OAI.ThorpNine.Dense.Thorp.pathWeight_sum line 75
  6. lemma OAI.ThorpNine.Dense.Thorp.withinWeight_sum_bound line 92
  7. def OAI.ThorpNine.Dense.Thorp.rotationCharge line 114
  8. lemma OAI.ThorpNine.Dense.Thorp.rotationCharge_mean_bound line 118
  9. lemma OAI.ThorpNine.Dense.Thorp.rotation_exp_bound line 136
  10. lemma OAI.ThorpNine.Dense.Thorp.mem_orbitSet line 158
  11. lemma OAI.ThorpNine.Dense.Thorp.orbitSet_nonempty line 163
  12. lemma OAI.ThorpNine.Dense.Thorp.orbitSet_eq line 166
  13. lemma OAI.ThorpNine.Dense.Thorp.orbitSet_apply line 172
  14. lemma OAI.ThorpNine.Dense.Thorp.orbitSet_eq_or_disjoint line 176
  15. lemma OAI.ThorpNine.Dense.Thorp.perm_minimalPeriod_pos line 187
  16. lemma OAI.ThorpNine.Dense.Thorp.orbitSet_card line 191
  17. def OAI.ThorpNine.Dense.Thorp.walkSet line 210
  18. lemma OAI.ThorpNine.Dense.Thorp.mem_walkSet line 214
  19. lemma OAI.ThorpNine.Dense.Thorp.walkSet_zero line 219
  20. lemma OAI.ThorpNine.Dense.Thorp.walkSet_succ_last line 223
  21. lemma OAI.ThorpNine.Dense.Thorp.walkSet_succ_first line 228
  22. lemma OAI.ThorpNine.Dense.Thorp.not_mem_short_walk line 242
  23. lemma OAI.ThorpNine.Dense.Thorp.walkSet_period line 251
  24. lemma OAI.ThorpNine.Dense.Thorp.walkSet_card line 265
  25. lemma OAI.ThorpNine.Dense.Thorp.walkSet_subset_orbit line 274
  26. def OAI.ThorpNine.Dense.Thorp.cycleTrace line 281
  27. lemma OAI.ThorpNine.Dense.Thorp.cycleTrace_walk line 286
  28. lemma OAI.ThorpNine.Dense.Thorp.cycleTrace_orbit line 320
  29. def OAI.ThorpNine.Dense.Thorp.exposedPaths line 342
  30. lemma OAI.ThorpNine.Dense.Thorp.exposedPaths_empty line 346
  31. lemma OAI.ThorpNine.Dense.Thorp.exposedPaths_insert line 350
  32. def OAI.ThorpNine.Dense.Thorp.terminalCharge line 355
  33. lemma OAI.ThorpNine.Dense.Thorp.QueryTree.followPath_stale_charge line 360
  34. lemma OAI.ThorpNine.Dense.Thorp.QueryTree.seekCycle_semantics line 372
  35. lemma OAI.ThorpNine.Dense.Thorp.QueryTree.seekCycle_orbit line 402
  36. lemma OAI.ThorpNine.Dense.Thorp.mem_exposedPaths line 417
  37. lemma OAI.ThorpNine.Dense.Thorp.terminalCharge_sum line 429
  38. def OAI.ThorpNine.Dense.Thorp.priorPaths line 451
  39. lemma OAI.ThorpNine.Dense.Thorp.mem_priorPaths line 454
  40. lemma OAI.ThorpNine.Dense.Thorp.terminalCharge_prior_sum line 459
  41. lemma OAI.ThorpNine.Dense.Thorp.rotationMeeting_eq_slot_sum line 476
  42. lemma OAI.ThorpNine.Dense.Thorp.rotationCharge_eq_terminal_sum line 528
  43. lemma OAI.ThorpNine.Dense.Thorp.priorPaths_zero line 535
  44. lemma OAI.ThorpNine.Dense.Thorp.priorPaths_succ line 540
  45. lemma OAI.ThorpNine.Dense.Thorp.priorPaths_disjoint line 555
  46. lemma OAI.ThorpNine.Dense.Thorp.QueryTree.seekCycles_owned line 567
  47. def OAI.ThorpNine.Dense.Thorp.ValidCycleSlots line 616
  48. abbrev OAI.ThorpNine.Dense.Thorp.CycleSlots line 622
  49. instance OAI.ThorpNine.Dense.Thorp.(instance at line 625) line 625
  50. lemma OAI.ThorpNine.Dense.Thorp.CycleSlots.terminal_nonempty line 628
  51. lemma OAI.ThorpNine.Dense.Thorp.owner_ext line 634
  52. abbrev OAI.ThorpNine.Dense.Thorp.RootedSlots line 646
  53. def OAI.ThorpNine.Dense.Thorp.rootedStart line 649
  54. lemma OAI.ThorpNine.Dense.Thorp.rootedStart_injective line 655
  55. lemma OAI.ThorpNine.Dense.Thorp.sum_comp_injective_le line 668
  56. lemma OAI.ThorpNine.Dense.Thorp.rooted_weight_sum_le line 676
  57. def OAI.ThorpNine.Dense.Thorp.rotationLower line 702
  58. def OAI.ThorpNine.Dense.Thorp.collectionWeight line 705
  59. lemma OAI.ThorpNine.Dense.Thorp.collectionWeight_pos line 708
  60. lemma OAI.ThorpNine.Dense.Thorp.collection_rotation_lower line 712
  61. lemma OAI.ThorpNine.Dense.Thorp.cycleSlots_weighted_moment line 740
  62. lemma OAI.ThorpNine.Dense.Thorp.cycleSlots_moment line 773
  63. lemma OAI.ThorpNine.Dense.Thorp.collectionWeight_eq_sqrt line 779
  64. lemma OAI.ThorpNine.Dense.Thorp.butterfly_cycleSlots_moment line 804
  65. abbrev OAI.ThorpNine.Dense.Thorp.SelectedCycle line 818
  66. instance OAI.ThorpNine.Dense.Thorp.(instance at line 821) line 821
  67. lemma OAI.ThorpNine.Dense.Thorp.SelectedCycle.nonempty line 824
  68. lemma OAI.ThorpNine.Dense.Thorp.SelectedCycle.orbit_eq line 830
  69. lemma OAI.ThorpNine.Dense.Thorp.SelectedCycle.eq_of_mem line 836
  70. abbrev OAI.ThorpNine.Dense.Thorp.SlotAssignment line 841
  71. instance OAI.ThorpNine.Dense.Thorp.(instance at line 844) line 844
  72. def OAI.ThorpNine.Dense.Thorp.slotsToAssignment line 847
  73. def OAI.ThorpNine.Dense.Thorp.assignmentOwner line 861
  74. lemma OAI.ThorpNine.Dense.Thorp.assignmentOwner_eq_some line 866