OAI/Probability/ThorpRouting/SparseSaving/AlternatingPerm.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.bipartitionFlip_injective line 14
2. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.card_opposite_le line 29
3. def OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.alternatingPerm line 36
4. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.alternatingPerm_flip line 43
5. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.alternating_step_sameCycle line 49
6. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.alternating_sameCycle_snd line 57
7. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.alternating_zero_sameCycle line 69
8. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.alternating_sameCycle_zero line 82
9. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.alternating_sameCycle_iff line 90
10. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.orbit_alternating line 98
11. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.boolFiber_childJoin line 104
12. def OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.projectCycle line 109
13. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.selected_alternating_eq line 120
14. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.projectCycle_injective line 128
15. lemma OAI.ThorpNine.SparseSaving.Thorp.CycleColoring.card_alternating_cycles_le line 134
16. lemma OAI.ThorpNine.SparseSaving.Thorp.mem_image_perm_iff line 145
17. lemma OAI.ThorpNine.SparseSaving.Thorp.card_childJoin line 155
18. lemma OAI.ThorpNine.SparseSaving.Thorp.alternating_internal line 168
19. lemma OAI.ThorpNine.SparseSaving.Thorp.alternating_boundary_card line 177
20. lemma OAI.ThorpNine.SparseSaving.Thorp.compatible_assignment_bound line 188
21. lemma OAI.ThorpNine.SparseSaving.Thorp.finiteMean_nonneg line 200
22. lemma OAI.ThorpNine.SparseSaving.Thorp.boolFiber_headTail line 204
23. lemma OAI.ThorpNine.SparseSaving.Thorp.prod_childMarks line 219
24. def OAI.ThorpNine.SparseSaving.Thorp.headAverage line 230
25. lemma OAI.ThorpNine.SparseSaving.Thorp.finiteMean_headAverage line 233
26. lemma OAI.ThorpNine.SparseSaving.Thorp.pairSwitch_product_bound line 241
27. lemma OAI.ThorpNine.SparseSaving.Thorp.butterflyPerm_step line 266
28. lemma OAI.ThorpNine.SparseSaving.Thorp.butterfly_product_bound line 281
29. def OAI.ThorpNine.SparseSaving.Thorp.inverseButterflyMarks line 334
30. lemma OAI.ThorpNine.SparseSaving.Thorp.inverseButterflyMarks_inclusion line 338
31. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.occupied line 363
32. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.mem_occupied line 367
33. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.required line 370
34. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.Compatible line 372
35. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.colors line 375
36. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.required_colors line 379
37. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.colors_compatible line 385
38. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.chosenCoin line 389
39. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.chosenCoin_apply line 394
40. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.colors_eq_iff line 401
41. instance OAI.ThorpNine.SparseSaving.Thorp.PairRouting.(instance at line 413) line 413
42. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.colors_probability line 416
43. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.Compatible.tail_injective line 430
44. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.childEmbedding line 441
45. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.lift line 445
46. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.sandwich line 451
47. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.ChildMatches line 454
48. instance OAI.ThorpNine.SparseSaving.Thorp.PairRouting.(instance at line 457) line 457
49. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.sandwich_matches_iff line 461
50. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.sandwich_probability line 472
51. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.childMatches_split line 502
52. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.tupleProbability line 518
53. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.childMatches_mean line 524
54. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.sandwich_mean line 542
55. abbrev OAI.ThorpNine.SparseSaving.Thorp.PairRouting.BothAssignments line 563
56. instance OAI.ThorpNine.SparseSaving.Thorp.PairRouting.(instance at line 566) line 566
57. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.labelSet line 569
58. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.alternatingProjection line 571
59. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.assignmentColoring line 573
60. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.assignmentColoring_injective line 612
61. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.bothAssignments_card line 622
62. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.occupied_labelSet line 635
63. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.image_snd_childJoin line 640
64. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.image_lift_childJoin line 645
65. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.occupied_lift_card line 651
66. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.bothAssignments_occupied_bound line 668
67. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.compatible_pairLayer_iff line 682
68. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.alternatingCycles line 696
69. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.occupied_eq_fibers line 701
70. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.card_labelSet line 707
71. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.occupied_card_double line 712
72. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.bothAssignments_exact_bound line 723
73. abbrev OAI.ThorpNine.SparseSaving.Thorp.PairRouting.Assignments line 743
74. instance OAI.ThorpNine.SparseSaving.Thorp.PairRouting.(instance at line 746) line 746
75. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.switchedEmbedding line 748
76. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.routedEmbedding line 751
77. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.occupied_pairLayer line 755
78. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.assignmentsEquiv line 758
79. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.assignments_actual_bound line 767
80. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.assignments_actual_exponent_nonneg line 775
81. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.compatibleSet line 785
82. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.mem_compatibleSet line 790
83. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.card_compatibleSet line 796
84. def OAI.ThorpNine.SparseSaving.Thorp.PairRouting.outerWeight line 801
85. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.outerWeight_pos line 805
86. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.sum_colors_factor line 810
87. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.sandwich_weighted_probability line 825
88. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.tupleProbability_nonneg line 852
89. lemma OAI.ThorpNine.SparseSaving.Thorp.PairRouting.sandwich_power_bound line 857