OAI/Probability/ThorpRouting/HighTail/ParallelFollow.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.HighTail.Thorp.parallel_entropy line 14
2. def OAI.ThorpNine.HighTail.Thorp.parallelFollow line 37
3. lemma OAI.ThorpNine.HighTail.Thorp.parallelFollow_succeeds line 42
4. lemma OAI.ThorpNine.HighTail.Thorp.parallelFollow_raw_charge line 48
5. lemma OAI.ThorpNine.HighTail.Thorp.parallelFollow_stale_charge line 54
6. def OAI.ThorpNine.HighTail.Thorp.closingDomain line 61
7. def OAI.ThorpNine.HighTail.Thorp.closingValue line 65
8. lemma OAI.ThorpNine.HighTail.Thorp.relabeled_endpoint_pair line 69
9. lemma OAI.ThorpNine.HighTail.Thorp.relabeled_endpoint_iff line 78
10. lemma OAI.ThorpNine.HighTail.Thorp.closingDomain_eq line 88
11. def OAI.ThorpNine.HighTail.Thorp.parallelClose line 93
12. lemma OAI.ThorpNine.HighTail.Thorp.parallelClose_succeeds line 100
13. lemma OAI.ThorpNine.HighTail.Thorp.parallelClose_raw_charge line 112
14. lemma OAI.ThorpNine.HighTail.Thorp.parallelClose_fresh_charge line 122
15. lemma OAI.ThorpNine.HighTail.Thorp.parallelClose_stale_charge line 133
16. def OAI.ThorpNine.HighTail.Thorp.parallelNetwork line 145
17. lemma OAI.ThorpNine.HighTail.Thorp.parallel_cycle_log_mgf line 163
18. lemma OAI.ThorpNine.HighTail.Thorp.butterfly_split line 172
19. def OAI.ThorpNine.HighTail.Thorp.splitSwitch line 198
20. lemma OAI.ThorpNine.HighTail.Thorp.assembleBits_eq line 242
21. def OAI.ThorpNine.HighTail.Thorp.splitCoinEquiv line 254
22. lemma OAI.ThorpNine.HighTail.Thorp.splitCoinEquiv_apply line 260
23. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_prod line 266
24. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_split line 271
25. def OAI.ThorpNine.HighTail.Thorp.freshPre line 286
26. def OAI.ThorpNine.HighTail.Thorp.freshPost line 290
27. lemma OAI.ThorpNine.HighTail.Thorp.exposed_perm_eq line 293
28. lemma OAI.ThorpNine.HighTail.Thorp.partially_exposed_cycle_log_mgf line 302
29. lemma OAI.ThorpNine.HighTail.Thorp.inclusionMoment_eq line 316
30. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_bool line 324
31. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_const line 328
32. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_pi_prod line 333
33. def OAI.ThorpNine.HighTail.Thorp.pairFiber line 341
34. lemma OAI.ThorpNine.HighTail.Thorp.prod_pairFiber line 344
35. lemma OAI.ThorpNine.HighTail.Thorp.fiber_average_bound line 354
36. lemma OAI.ThorpNine.HighTail.Thorp.CylinderBound.fair_parallel line 365
37. lemma OAI.ThorpNine.HighTail.Thorp.subset_pairLayer_image_iff line 391
38. def OAI.ThorpNine.HighTail.Thorp.fairSetLayer line 402
39. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_comm line 405
40. lemma OAI.ThorpNine.HighTail.Thorp.inclusionMoment_fairSetLayer line 410
41. lemma OAI.ThorpNine.HighTail.Thorp.inclusionMoment_fairSetLayer_singleton line 425
42. lemma OAI.ThorpNine.HighTail.Thorp.cylinder_fairSetLayer line 436
43. lemma OAI.ThorpNine.HighTail.Thorp.subset_image_equiv_iff line 453
44. lemma OAI.ThorpNine.HighTail.Thorp.inclusionMoment_image_equiv line 464
45. lemma OAI.ThorpNine.HighTail.Thorp.cylinder_image_equiv line 473
46. lemma OAI.ThorpNine.HighTail.Thorp.inclusionMoment_comp_equiv line 483
47. lemma OAI.ThorpNine.HighTail.Thorp.cylinder_comp_equiv line 491
48. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_prod_mul line 499
49. def OAI.ThorpNine.HighTail.Thorp.childJoin line 509
50. lemma OAI.ThorpNine.HighTail.Thorp.mem_childJoin line 512
51. def OAI.ThorpNine.HighTail.Thorp.boolFiber line 516
52. lemma OAI.ThorpNine.HighTail.Thorp.mem_boolFiber line 519
53. lemma OAI.ThorpNine.HighTail.Thorp.childJoin_boolFiber line 531
54. lemma OAI.ThorpNine.HighTail.Thorp.subset_childJoin_iff line 537
55. lemma OAI.ThorpNine.HighTail.Thorp.prod_childJoin line 552
56. lemma OAI.ThorpNine.HighTail.Thorp.prod_boolFibers line 565
57. lemma OAI.ThorpNine.HighTail.Thorp.inclusionMoment_childJoin line 570
58. lemma OAI.ThorpNine.HighTail.Thorp.cylinder_childJoin line 582
59. lemma OAI.ThorpNine.HighTail.Thorp.childMarks_join line 613
60. def OAI.ThorpNine.HighTail.Thorp.butterflyMarks line 634
61. lemma OAI.ThorpNine.HighTail.Thorp.butterflyMarks_succ line 638
62. lemma OAI.ThorpNine.HighTail.Thorp.butterflyMarks_cylinder line 665
63. lemma OAI.ThorpNine.HighTail.Thorp.indicator_mem_image_perm line 682
64. lemma OAI.ThorpNine.HighTail.Thorp.butterflyMarks_singleton line 701
65. lemma OAI.ThorpNine.HighTail.Thorp.butterflyMarks_inclusion line 710
66. abbrev OAI.ThorpNine.HighTail.Thorp.CycleColoring.Coloring line 718
67. instance OAI.ThorpNine.HighTail.Thorp.CycleColoring.(instance at line 722) line 722
68. def OAI.ThorpNine.HighTail.Thorp.CycleColoring.boundary line 725
69. def OAI.ThorpNine.HighTail.Thorp.CycleColoring.root line 728
70. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.root_mem line 731
71. abbrev OAI.ThorpNine.HighTail.Thorp.CycleColoring.Seed line 734
72. def OAI.ThorpNine.HighTail.Thorp.CycleColoring.record line 737
73. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.orbit_subset_of_predecessor_closed line 741
74. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.record_injective line 752
75. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.card_coloring_le line 783
76. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.boundary_card line 790
77. lemma OAI.ThorpNine.HighTail.Thorp.CycleColoring.card_coloring_le_edges line 797
78. abbrev OAI.ThorpNine.HighTail.Thorp.CycleColoring.OppositeColoring line 804
79. instance OAI.ThorpNine.HighTail.Thorp.CycleColoring.(instance at line 808) line 808
80. def OAI.ThorpNine.HighTail.Thorp.CycleColoring.bipartitionFlip line 811