OAI/Probability/ThorpRouting/Casimir/ParallelFollow.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Casimir.Thorp.parallel_entropy line 14
2. def OAI.ThorpNine.Casimir.Thorp.parallelFollow line 37
3. lemma OAI.ThorpNine.Casimir.Thorp.parallelFollow_succeeds line 42
4. lemma OAI.ThorpNine.Casimir.Thorp.parallelFollow_raw_charge line 48
5. lemma OAI.ThorpNine.Casimir.Thorp.parallelFollow_stale_charge line 54
6. def OAI.ThorpNine.Casimir.Thorp.closingDomain line 61
7. def OAI.ThorpNine.Casimir.Thorp.closingValue line 65
8. lemma OAI.ThorpNine.Casimir.Thorp.relabeled_endpoint_pair line 69
9. lemma OAI.ThorpNine.Casimir.Thorp.relabeled_endpoint_iff line 78
10. lemma OAI.ThorpNine.Casimir.Thorp.closingDomain_eq line 88
11. def OAI.ThorpNine.Casimir.Thorp.parallelClose line 93
12. lemma OAI.ThorpNine.Casimir.Thorp.parallelClose_succeeds line 100
13. lemma OAI.ThorpNine.Casimir.Thorp.parallelClose_raw_charge line 112
14. lemma OAI.ThorpNine.Casimir.Thorp.parallelClose_fresh_charge line 122
15. lemma OAI.ThorpNine.Casimir.Thorp.parallelClose_stale_charge line 133
16. def OAI.ThorpNine.Casimir.Thorp.parallelNetwork line 145
17. lemma OAI.ThorpNine.Casimir.Thorp.parallel_cycle_log_mgf line 163
18. def OAI.ThorpNine.Casimir.Thorp.cardSplit line 172
19. def OAI.ThorpNine.Casimir.Thorp.assembleBits line 192
20. lemma OAI.ThorpNine.Casimir.Thorp.butterfly_split line 199
21. def OAI.ThorpNine.Casimir.Thorp.splitSwitch line 225
22. lemma OAI.ThorpNine.Casimir.Thorp.assembleBits_eq line 269
23. def OAI.ThorpNine.Casimir.Thorp.splitCoinEquiv line 281
24. lemma OAI.ThorpNine.Casimir.Thorp.splitCoinEquiv_apply line 287
25. lemma OAI.ThorpNine.Casimir.Thorp.finiteMean_prod line 293
26. lemma OAI.ThorpNine.Casimir.Thorp.finiteMean_split line 298
27. def OAI.ThorpNine.Casimir.Thorp.freshPre line 313
28. def OAI.ThorpNine.Casimir.Thorp.freshPost line 317
29. lemma OAI.ThorpNine.Casimir.Thorp.exposed_perm_eq line 320
30. lemma OAI.ThorpNine.Casimir.Thorp.partially_exposed_cycle_log_mgf line 329
31. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_eq line 343
32. lemma OAI.ThorpNine.Casimir.Thorp.finiteMean_bool line 351
33. lemma OAI.ThorpNine.Casimir.Thorp.finiteMean_const line 355
34. lemma OAI.ThorpNine.Casimir.Thorp.finiteMean_pi_prod line 360
35. def OAI.ThorpNine.Casimir.Thorp.pairLayer line 368
36. def OAI.ThorpNine.Casimir.Thorp.pairFiber line 380
37. lemma OAI.ThorpNine.Casimir.Thorp.prod_pairFiber line 383
38. lemma OAI.ThorpNine.Casimir.Thorp.fiber_average_bound line 393
39. lemma OAI.ThorpNine.Casimir.Thorp.CylinderBound.fair_parallel line 404
40. lemma OAI.ThorpNine.Casimir.Thorp.subset_pairLayer_image_iff line 430
41. def OAI.ThorpNine.Casimir.Thorp.fairSetLayer line 441
42. lemma OAI.ThorpNine.Casimir.Thorp.finiteMean_comm line 444
43. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_fairSetLayer line 449
44. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_fairSetLayer_singleton line 464
45. lemma OAI.ThorpNine.Casimir.Thorp.cylinder_fairSetLayer line 475
46. lemma OAI.ThorpNine.Casimir.Thorp.subset_image_equiv_iff line 492
47. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_image_equiv line 503
48. lemma OAI.ThorpNine.Casimir.Thorp.cylinder_image_equiv line 512
49. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_comp_equiv line 522
50. lemma OAI.ThorpNine.Casimir.Thorp.cylinder_comp_equiv line 530
51. lemma OAI.ThorpNine.Casimir.Thorp.finiteMean_prod_mul line 538
52. def OAI.ThorpNine.Casimir.Thorp.childJoin line 548
53. lemma OAI.ThorpNine.Casimir.Thorp.mem_childJoin line 551
54. def OAI.ThorpNine.Casimir.Thorp.boolFiber line 555
55. lemma OAI.ThorpNine.Casimir.Thorp.mem_boolFiber line 558
56. lemma OAI.ThorpNine.Casimir.Thorp.childJoin_boolFiber line 570
57. lemma OAI.ThorpNine.Casimir.Thorp.subset_childJoin_iff line 576
58. lemma OAI.ThorpNine.Casimir.Thorp.prod_childJoin line 591
59. lemma OAI.ThorpNine.Casimir.Thorp.prod_boolFibers line 604
60. lemma OAI.ThorpNine.Casimir.Thorp.inclusionMoment_childJoin line 609
61. lemma OAI.ThorpNine.Casimir.Thorp.cylinder_childJoin line 621
62. def OAI.ThorpNine.Casimir.Thorp.coinStepEquiv line 652
63. def OAI.ThorpNine.Casimir.Thorp.headTailEquiv line 666
64. lemma OAI.ThorpNine.Casimir.Thorp.childMarks_join line 669
65. def OAI.ThorpNine.Casimir.Thorp.butterflyMarks line 690
66. lemma OAI.ThorpNine.Casimir.Thorp.butterflyMarks_succ line 694
67. lemma OAI.ThorpNine.Casimir.Thorp.butterflyMarks_cylinder line 721
68. lemma OAI.ThorpNine.Casimir.Thorp.indicator_mem_image_perm line 738
69. lemma OAI.ThorpNine.Casimir.Thorp.butterflyMarks_singleton line 757
70. lemma OAI.ThorpNine.Casimir.Thorp.butterflyMarks_inclusion line 766
71. abbrev OAI.ThorpNine.Casimir.Thorp.CycleColoring.Coloring line 774
72. instance OAI.ThorpNine.Casimir.Thorp.CycleColoring.(instance at line 778) line 778
73. def OAI.ThorpNine.Casimir.Thorp.CycleColoring.boundary line 781
74. def OAI.ThorpNine.Casimir.Thorp.CycleColoring.root line 784
75. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.root_mem line 787
76. abbrev OAI.ThorpNine.Casimir.Thorp.CycleColoring.Seed line 790
77. def OAI.ThorpNine.Casimir.Thorp.CycleColoring.record line 793
78. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.orbit_subset_of_predecessor_closed line 797
79. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.record_injective line 808
80. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.card_coloring_le line 839
81. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.boundary_card line 846
82. lemma OAI.ThorpNine.Casimir.Thorp.CycleColoring.card_coloring_le_edges line 853
83. abbrev OAI.ThorpNine.Casimir.Thorp.CycleColoring.OppositeColoring line 860
84. instance OAI.ThorpNine.Casimir.Thorp.CycleColoring.(instance at line 864) line 864
85. def OAI.ThorpNine.Casimir.Thorp.CycleColoring.bipartitionFlip line 867