OAI/Probability/ThorpRouting/HighTail/ProjectCycle.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.bipartitionFlip_injective line 14
2. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.card_opposite_le line 29
3. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.alternatingPerm_flip line 37
4. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.alternating_step_sameCycle line 43
5. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.alternating_sameCycle_snd line 51
6. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.alternating_zero_sameCycle line 63
7. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.alternating_sameCycle_zero line 76
8. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.alternating_sameCycle_iff line 84
9. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.orbit_alternating line 92
10. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.boolFiber_childJoin line 98
11. def OAI.ThorpNine.HighTail.Thorp.CycleColoring.projectCycle line 103
12. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.selected_alternating_eq line 114
13. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.projectCycle_injective line 122
14. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.card_alternating_cycles_le line 128
15. lemma OAI.ThorpNine.HighTail.Thorp.mem_image_perm_iff line 139
16. lemma OAI.ThorpNine.HighTail.Thorp.card_childJoin line 149
17. lemma OAI.ThorpNine.HighTail.Thorp.alternating_internal line 162
18. lemma OAI.ThorpNine.HighTail.Thorp.alternating_boundary_card line 171
19. lemma OAI.ThorpNine.HighTail.Thorp.compatible_assignment_bound line 182
20. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_nonneg line 194
21. lemma OAI.ThorpNine.HighTail.Thorp.boolFiber_headTail line 198
22. lemma OAI.ThorpNine.HighTail.Thorp.prod_childMarks line 213
23. def OAI.ThorpNine.HighTail.Thorp.headAverage line 224
24. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_headAverage line 227
25. lemma OAI.ThorpNine.HighTail.Thorp.pairSwitch_product_bound line 235
26. lemma OAI.ThorpNine.HighTail.Thorp.butterflyPerm_step line 260
27. lemma OAI.ThorpNine.HighTail.Thorp.butterfly_product_bound line 275
28. def OAI.ThorpNine.HighTail.Thorp.inverseButterflyMarks line 328
29. lemma OAI.ThorpNine.HighTail.Thorp.inverseButterflyMarks_inclusion line 332
30. def OAI.ThorpNine.HighTail.Thorp.PairRouting.occupied line 357
31. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.mem_occupied line 361
32. def OAI.ThorpNine.HighTail.Thorp.PairRouting.chosenCoin line 364
33. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.chosenCoin_apply line 369
34. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.colors_eq_iff line 376
35. instance OAI.ThorpNine.HighTail.Thorp.PairRouting.(instance at line 388) line 388
36. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.colors_probability line 391
37. def OAI.ThorpNine.HighTail.Thorp.PairRouting.lift line 405
38. def OAI.ThorpNine.HighTail.Thorp.PairRouting.sandwich line 411
39. def OAI.ThorpNine.HighTail.Thorp.PairRouting.ChildMatches line 414
40. instance OAI.ThorpNine.HighTail.Thorp.PairRouting.(instance at line 417) line 417
41. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.sandwich_matches_iff line 421
42. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.sandwich_probability line 432
43. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.childMatches_split line 462
44. def OAI.ThorpNine.HighTail.Thorp.PairRouting.tupleProbability line 478
45. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.childMatches_mean line 484
46. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.sandwich_mean line 502
47. abbrev OAI.ThorpNine.HighTail.Thorp.PairRouting.BothAssignments line 523
48. instance OAI.ThorpNine.HighTail.Thorp.PairRouting.(instance at line 526) line 526
49. def OAI.ThorpNine.HighTail.Thorp.PairRouting.assignmentColoring line 529
50. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.assignmentColoring_injective line 568
51. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.bothAssignments_card line 578
52. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.occupied_labelSet line 591
53. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.image_snd_childJoin line 596
54. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.image_lift_childJoin line 601
55. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.occupied_lift_card line 607
56. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.bothAssignments_occupied_bound line 624
57. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.compatible_pairLayer_iff line 638
58. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.occupied_eq_fibers line 653
59. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.card_labelSet line 659
60. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.occupied_card_double line 664
61. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.bothAssignments_exact_bound line 675
62. abbrev OAI.ThorpNine.HighTail.Thorp.PairRouting.Assignments line 695
63. instance OAI.ThorpNine.HighTail.Thorp.PairRouting.(instance at line 698) line 698
64. def OAI.ThorpNine.HighTail.Thorp.PairRouting.routedEmbedding line 700
65. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.occupied_pairLayer line 704
66. def OAI.ThorpNine.HighTail.Thorp.PairRouting.assignmentsEquiv line 707
67. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.assignments_actual_bound line 716
68. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.assignments_actual_exponent_nonneg line 724
69. def OAI.ThorpNine.HighTail.Thorp.PairRouting.compatibleSet line 734
70. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.mem_compatibleSet line 739
71. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.card_compatibleSet line 745
72. def OAI.ThorpNine.HighTail.Thorp.PairRouting.outerWeight line 750
73. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.outerWeight_pos line 754
74. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.sum_colors_factor line 759
75. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.sandwich_weighted_probability line 774
76. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.tupleProbability_nonneg line 801