OAI/Probability/ThorpRouting/Dense/ParallelFollow.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Dense.Thorp.parallel_entropy line 14
  2. def OAI.ThorpNine.Dense.Thorp.parallelFollow line 37
  3. lemma OAI.ThorpNine.Dense.Thorp.parallelFollow_succeeds line 42
  4. lemma OAI.ThorpNine.Dense.Thorp.parallelFollow_raw_charge line 48
  5. lemma OAI.ThorpNine.Dense.Thorp.parallelFollow_stale_charge line 54
  6. def OAI.ThorpNine.Dense.Thorp.closingDomain line 61
  7. def OAI.ThorpNine.Dense.Thorp.closingValue line 65
  8. lemma OAI.ThorpNine.Dense.Thorp.relabeled_endpoint_pair line 69
  9. lemma OAI.ThorpNine.Dense.Thorp.relabeled_endpoint_iff line 78
  10. lemma OAI.ThorpNine.Dense.Thorp.closingDomain_eq line 88
  11. def OAI.ThorpNine.Dense.Thorp.parallelClose line 93
  12. lemma OAI.ThorpNine.Dense.Thorp.parallelClose_succeeds line 100
  13. lemma OAI.ThorpNine.Dense.Thorp.parallelClose_raw_charge line 112
  14. lemma OAI.ThorpNine.Dense.Thorp.parallelClose_fresh_charge line 122
  15. lemma OAI.ThorpNine.Dense.Thorp.parallelClose_stale_charge line 133
  16. def OAI.ThorpNine.Dense.Thorp.parallelNetwork line 145
  17. lemma OAI.ThorpNine.Dense.Thorp.parallel_cycle_log_mgf line 163
  18. def OAI.ThorpNine.Dense.Thorp.cardSplit line 172
  19. def OAI.ThorpNine.Dense.Thorp.assembleBits line 192
  20. lemma OAI.ThorpNine.Dense.Thorp.butterfly_split line 199
  21. def OAI.ThorpNine.Dense.Thorp.splitSwitch line 225
  22. lemma OAI.ThorpNine.Dense.Thorp.assembleBits_eq line 269
  23. def OAI.ThorpNine.Dense.Thorp.splitCoinEquiv line 281
  24. lemma OAI.ThorpNine.Dense.Thorp.splitCoinEquiv_apply line 287
  25. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_prod line 293
  26. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_split line 298
  27. def OAI.ThorpNine.Dense.Thorp.freshPre line 313
  28. def OAI.ThorpNine.Dense.Thorp.freshPost line 317
  29. lemma OAI.ThorpNine.Dense.Thorp.exposed_perm_eq line 320
  30. lemma OAI.ThorpNine.Dense.Thorp.partially_exposed_cycle_log_mgf line 329
  31. lemma OAI.ThorpNine.Dense.Thorp.inclusionMoment_eq line 343
  32. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_bool line 351
  33. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_const line 355
  34. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_pi_prod line 360
  35. def OAI.ThorpNine.Dense.Thorp.pairFiber line 368
  36. lemma OAI.ThorpNine.Dense.Thorp.prod_pairFiber line 371
  37. lemma OAI.ThorpNine.Dense.Thorp.fiber_average_bound line 381
  38. lemma OAI.ThorpNine.Dense.Thorp.CylinderBound.fair_parallel line 392
  39. lemma OAI.ThorpNine.Dense.Thorp.subset_pairLayer_image_iff line 418
  40. def OAI.ThorpNine.Dense.Thorp.fairSetLayer line 429
  41. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_comm line 432
  42. lemma OAI.ThorpNine.Dense.Thorp.inclusionMoment_fairSetLayer line 437
  43. lemma OAI.ThorpNine.Dense.Thorp.inclusionMoment_fairSetLayer_singleton line 452
  44. lemma OAI.ThorpNine.Dense.Thorp.cylinder_fairSetLayer line 463
  45. lemma OAI.ThorpNine.Dense.Thorp.subset_image_equiv_iff line 480
  46. lemma OAI.ThorpNine.Dense.Thorp.inclusionMoment_image_equiv line 491
  47. lemma OAI.ThorpNine.Dense.Thorp.cylinder_image_equiv line 500
  48. lemma OAI.ThorpNine.Dense.Thorp.inclusionMoment_comp_equiv line 510
  49. lemma OAI.ThorpNine.Dense.Thorp.cylinder_comp_equiv line 518
  50. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_prod_mul line 526
  51. def OAI.ThorpNine.Dense.Thorp.childJoin line 536
  52. lemma OAI.ThorpNine.Dense.Thorp.mem_childJoin line 539
  53. def OAI.ThorpNine.Dense.Thorp.boolFiber line 543
  54. lemma OAI.ThorpNine.Dense.Thorp.mem_boolFiber line 546
  55. lemma OAI.ThorpNine.Dense.Thorp.childJoin_boolFiber line 558
  56. lemma OAI.ThorpNine.Dense.Thorp.subset_childJoin_iff line 564
  57. lemma OAI.ThorpNine.Dense.Thorp.prod_childJoin line 579
  58. lemma OAI.ThorpNine.Dense.Thorp.prod_boolFibers line 592
  59. lemma OAI.ThorpNine.Dense.Thorp.inclusionMoment_childJoin line 597
  60. lemma OAI.ThorpNine.Dense.Thorp.cylinder_childJoin line 609
  61. lemma OAI.ThorpNine.Dense.Thorp.childMarks_join line 640
  62. def OAI.ThorpNine.Dense.Thorp.butterflyMarks line 661
  63. lemma OAI.ThorpNine.Dense.Thorp.butterflyMarks_succ line 665
  64. lemma OAI.ThorpNine.Dense.Thorp.butterflyMarks_cylinder line 692
  65. lemma OAI.ThorpNine.Dense.Thorp.indicator_mem_image_perm line 709
  66. lemma OAI.ThorpNine.Dense.Thorp.butterflyMarks_singleton line 728
  67. lemma OAI.ThorpNine.Dense.Thorp.butterflyMarks_inclusion line 737
  68. abbrev OAI.ThorpNine.Dense.Thorp.CycleColoring.Coloring line 745
  69. instance OAI.ThorpNine.Dense.Thorp.CycleColoring.(instance at line 749) line 749
  70. def OAI.ThorpNine.Dense.Thorp.CycleColoring.boundary line 752
  71. def OAI.ThorpNine.Dense.Thorp.CycleColoring.root line 755
  72. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.root_mem line 758
  73. abbrev OAI.ThorpNine.Dense.Thorp.CycleColoring.Seed line 761
  74. def OAI.ThorpNine.Dense.Thorp.CycleColoring.record line 764
  75. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.orbit_subset_of_predecessor_closed line 768
  76. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.record_injective line 779
  77. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.card_coloring_le line 810
  78. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.boundary_card line 817
  79. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.card_coloring_le_edges line 824
  80. abbrev OAI.ThorpNine.Dense.Thorp.CycleColoring.OppositeColoring line 831
  81. instance OAI.ThorpNine.Dense.Thorp.CycleColoring.(instance at line 835) line 835
  82. def OAI.ThorpNine.Dense.Thorp.CycleColoring.bipartitionFlip line 838