OAI/Probability/ThorpRouting/Contact/PriorPaths.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.mem_exposedPaths line 14
2. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.terminalCharge_sum line 26
3. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.priorPaths line 48
4. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.mem_priorPaths line 52
5. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.terminalCharge_prior_sum line 57
6. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.rotationMeeting_eq_slot_sum line 74
7. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.rotationCharge_eq_terminal_sum line 126
8. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.priorPaths_zero line 134
9. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.priorPaths_succ line 139
10. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.priorPaths_disjoint line 155
11. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.QueryTree.seekCycles_owned line 168
12. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.ValidCycleSlots line 216
13. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.CycleSlots line 222
14. instance OAI.ThorpNine.Contact.Thorp.RoutingNetwork.(instance at line 225) line 225
15. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.CycleSlots.terminal_nonempty line 228
16. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.owner_ext line 235
17. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.RootedSlots line 247
18. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.rootedStart line 250
19. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.rootedStart_injective line 256
20. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.rooted_weight_sum_le line 269
21. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.collection_rotation_lower line 295
22. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.cycleSlots_weighted_moment line 323
23. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.cycleSlots_moment line 356
24. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.butterfly_cycleSlots_moment line 362
25. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.SelectedCycle line 377
26. instance OAI.ThorpNine.Contact.Thorp.RoutingNetwork.(instance at line 380) line 380
27. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.SelectedCycle.nonempty line 383
28. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.SelectedCycle.orbit_eq line 389
29. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.SelectedCycle.eq_of_mem line 395
30. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.SlotAssignment line 400
31. instance OAI.ThorpNine.Contact.Thorp.RoutingNetwork.(instance at line 403) line 403
32. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.slotsToAssignment line 406
33. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.assignmentOwner line 420
34. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.assignmentOwner_eq_some line 425
35. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.assignmentOwner_fiber line 443
36. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.assignmentToSlots line 448
37. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.cycleSlotsEquivAssignments line 462
38. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.LengthClass line 483
39. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.slotClass line 485
40. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.SlotsOfLength line 488
41. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.CyclesOfLength line 489
42. instance OAI.ThorpNine.Contact.Thorp.RoutingNetwork.(instance at line 492) line 492
43. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.GroupedAssignments line 495
44. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.assignmentToGroups line 498
45. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.groupsEmbedding line 503
46. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.groupsToAssignment line 510
47. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.assignmentEquivGroups line 515
48. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.card_cycleSlots_factorial line 530
49. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.butterfly_factorial_moment line 539
50. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.assignmentRelabel line 553
51. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.card_cycleSlots_relabel line 562
52. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.butterfly_cycleSlots_moment_all line 568
53. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.ShortCycle line 578
54. instance OAI.ThorpNine.Contact.Thorp.RoutingNetwork.(instance at line 581) line 581
55. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.shortCycleLength line 584
56. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.shortCycleLength_add_one line 588
57. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.shortEmbeddingEquiv line 594
58. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.shortCycle_factorial_eq line 620
59. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.butterfly_shortCycle_moment line 635
60. def OAI.ThorpNine.Contact.Thorp.RoutingNetwork.cycleMass line 654
61. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.cycleMass_le line 657
62. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.shortCycle_card_le line 675
63. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.butterfly_shortCycle_mgf line 684
64. abbrev OAI.ThorpNine.Contact.Thorp.RoutingNetwork.LongCycle line 696
65. instance OAI.ThorpNine.Contact.Thorp.RoutingNetwork.(instance at line 698) line 698
66. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.selectedCycle_card_split line 701
67. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.longCycle_card_bound line 707
68. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.longCycle_pow_bound line 723
69. lemma OAI.ThorpNine.Contact.Thorp.RoutingNetwork.butterfly_cycle_log_mgf line 736
70. def OAI.ThorpNine.Contact.Thorp.parallelPerm line 786
71. def OAI.ThorpNine.Contact.Thorp.relabeledPerm line 792
72. def OAI.ThorpNine.Contact.Thorp.parallelPath line 796
73. def OAI.ThorpNine.Contact.Thorp.parallelUsers line 802
74. lemma OAI.ThorpNine.Contact.Thorp.parallelUsers_ne line 808
75. lemma OAI.ThorpNine.Contact.Thorp.mem_parallelPath line 814
76. lemma OAI.ThorpNine.Contact.Thorp.card_parallelPath line 847
77. def OAI.ThorpNine.Contact.Thorp.blockMarks line 852
78. lemma OAI.ThorpNine.Contact.Thorp.mem_blockMarks line 856
79. lemma OAI.ThorpNine.Contact.Thorp.sum_card_blockMarks line 862
80. lemma OAI.ThorpNine.Contact.Thorp.card_blockMarks_le line 873