OAI/Probability/ThorpRouting/HighTail/PriorPaths.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.mem_exposedPaths line 14
2. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.terminalCharge_sum line 26
3. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.priorPaths line 48
4. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.mem_priorPaths line 52
5. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.terminalCharge_prior_sum line 57
6. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.rotationMeeting_eq_slot_sum line 74
7. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.rotationCharge_eq_terminal_sum line 126
8. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.priorPaths_zero line 134
9. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.priorPaths_succ line 139
10. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.priorPaths_disjoint line 155
11. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.QueryTree.seekCycles_owned line 168
12. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.ValidCycleSlots line 216
13. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.CycleSlots line 222
14. instance OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.(instance at line 225) line 225
15. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.CycleSlots.terminal_nonempty line 228
16. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.owner_ext line 235
17. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.RootedSlots line 247
18. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.rootedStart line 250
19. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.rootedStart_injective line 256
20. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.rooted_weight_sum_le line 269
21. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.collection_rotation_lower line 295
22. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.cycleSlots_weighted_moment line 323
23. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.cycleSlots_moment line 356
24. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.butterfly_cycleSlots_moment line 362
25. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.SelectedCycle.nonempty line 377
26. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.SelectedCycle.orbit_eq line 383
27. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.SelectedCycle.eq_of_mem line 389
28. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.SlotAssignment line 394
29. instance OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.(instance at line 397) line 397
30. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.slotsToAssignment line 400
31. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.assignmentOwner line 414
32. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.assignmentOwner_eq_some line 419
33. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.assignmentOwner_fiber line 437
34. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.assignmentToSlots line 442
35. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.cycleSlotsEquivAssignments line 456
36. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.LengthClass line 477
37. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.slotClass line 479
38. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.SlotsOfLength line 482
39. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.CyclesOfLength line 483
40. instance OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.(instance at line 486) line 486
41. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.GroupedAssignments line 489
42. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.assignmentToGroups line 492
43. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.groupsEmbedding line 497
44. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.groupsToAssignment line 504
45. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.assignmentEquivGroups line 509
46. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.card_cycleSlots_factorial line 524
47. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.butterfly_factorial_moment line 533
48. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.assignmentRelabel line 547
49. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.card_cycleSlots_relabel line 556
50. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.butterfly_cycleSlots_moment_all line 562
51. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.ShortCycle line 572
52. instance OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.(instance at line 575) line 575
53. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.shortCycleLength line 578
54. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.shortCycleLength_add_one line 582
55. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.shortEmbeddingEquiv line 588
56. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.shortCycle_factorial_eq line 614
57. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.butterfly_shortCycle_moment line 629
58. def OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.cycleMass line 648
59. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.cycleMass_le line 651
60. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.shortCycle_card_le line 669
61. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.butterfly_shortCycle_mgf line 678
62. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.LongCycle line 690
63. instance OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.(instance at line 692) line 692
64. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.selectedCycle_card_split line 695
65. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.longCycle_card_bound line 701
66. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.longCycle_pow_bound line 717
67. lemma OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.butterfly_cycle_log_mgf line 730
68. def OAI.ThorpNine.HighTail.Thorp.parallelPerm line 780
69. def OAI.ThorpNine.HighTail.Thorp.relabeledPerm line 786
70. def OAI.ThorpNine.HighTail.Thorp.parallelPath line 790
71. def OAI.ThorpNine.HighTail.Thorp.parallelUsers line 796
72. lemma OAI.ThorpNine.HighTail.Thorp.parallelUsers_ne line 802
73. lemma OAI.ThorpNine.HighTail.Thorp.mem_parallelPath line 808
74. lemma OAI.ThorpNine.HighTail.Thorp.card_parallelPath line 841
75. def OAI.ThorpNine.HighTail.Thorp.blockMarks line 846
76. lemma OAI.ThorpNine.HighTail.Thorp.mem_blockMarks line 850
77. lemma OAI.ThorpNine.HighTail.Thorp.sum_card_blockMarks line 856
78. lemma OAI.ThorpNine.HighTail.Thorp.card_blockMarks_le line 867