OAI/Probability/ThorpRouting/Smoothing/AlternatingPerm.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

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