OAI/Probability/ThorpRouting/Dense/ProjectCycle.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.bipartitionFlip_injective line 14
  2. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.card_opposite_le line 29
  3. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.alternatingPerm_flip line 37
  4. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.alternating_step_sameCycle line 43
  5. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.alternating_sameCycle_snd line 51
  6. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.alternating_zero_sameCycle line 63
  7. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.alternating_sameCycle_zero line 76
  8. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.alternating_sameCycle_iff line 84
  9. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.orbit_alternating line 92
  10. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.boolFiber_childJoin line 98
  11. def OAI.ThorpNine.Dense.Thorp.CycleColoring.projectCycle line 103
  12. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.selected_alternating_eq line 114
  13. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.projectCycle_injective line 122
  14. lemma OAI.ThorpNine.Dense.Thorp.CycleColoring.card_alternating_cycles_le line 128
  15. lemma OAI.ThorpNine.Dense.Thorp.mem_image_perm_iff line 139
  16. lemma OAI.ThorpNine.Dense.Thorp.card_childJoin line 149
  17. lemma OAI.ThorpNine.Dense.Thorp.alternating_internal line 162
  18. lemma OAI.ThorpNine.Dense.Thorp.alternating_boundary_card line 171
  19. lemma OAI.ThorpNine.Dense.Thorp.compatible_assignment_bound line 182
  20. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_nonneg line 194
  21. lemma OAI.ThorpNine.Dense.Thorp.boolFiber_headTail line 198
  22. lemma OAI.ThorpNine.Dense.Thorp.prod_childMarks line 213
  23. def OAI.ThorpNine.Dense.Thorp.headAverage line 224
  24. lemma OAI.ThorpNine.Dense.Thorp.finiteMean_headAverage line 227
  25. lemma OAI.ThorpNine.Dense.Thorp.pairSwitch_product_bound line 235
  26. lemma OAI.ThorpNine.Dense.Thorp.butterflyPerm_step line 260
  27. lemma OAI.ThorpNine.Dense.Thorp.butterfly_product_bound line 275
  28. def OAI.ThorpNine.Dense.Thorp.inverseButterflyMarks line 328
  29. lemma OAI.ThorpNine.Dense.Thorp.inverseButterflyMarks_inclusion line 332
  30. def OAI.ThorpNine.Dense.Thorp.PairRouting.occupied line 357
  31. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.mem_occupied line 361
  32. def OAI.ThorpNine.Dense.Thorp.PairRouting.chosenCoin line 364
  33. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.chosenCoin_apply line 369
  34. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.colors_eq_iff line 376
  35. instance OAI.ThorpNine.Dense.Thorp.PairRouting.(instance at line 388) line 388
  36. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.colors_probability line 391
  37. def OAI.ThorpNine.Dense.Thorp.PairRouting.lift line 405
  38. def OAI.ThorpNine.Dense.Thorp.PairRouting.sandwich line 411
  39. def OAI.ThorpNine.Dense.Thorp.PairRouting.ChildMatches line 414
  40. instance OAI.ThorpNine.Dense.Thorp.PairRouting.(instance at line 417) line 417
  41. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.sandwich_matches_iff line 421
  42. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.sandwich_probability line 432
  43. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.childMatches_split line 462
  44. def OAI.ThorpNine.Dense.Thorp.PairRouting.tupleProbability line 478
  45. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.childMatches_mean line 484
  46. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.sandwich_mean line 502
  47. abbrev OAI.ThorpNine.Dense.Thorp.PairRouting.BothAssignments line 523
  48. instance OAI.ThorpNine.Dense.Thorp.PairRouting.(instance at line 526) line 526
  49. def OAI.ThorpNine.Dense.Thorp.PairRouting.assignmentColoring line 529
  50. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.assignmentColoring_injective line 568
  51. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.bothAssignments_card line 578
  52. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.occupied_labelSet line 591
  53. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.image_snd_childJoin line 596
  54. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.image_lift_childJoin line 601
  55. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.occupied_lift_card line 607
  56. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.bothAssignments_occupied_bound line 624
  57. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.compatible_pairLayer_iff line 638
  58. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.occupied_eq_fibers line 653
  59. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.card_labelSet line 659
  60. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.occupied_card_double line 664
  61. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.bothAssignments_exact_bound line 675
  62. abbrev OAI.ThorpNine.Dense.Thorp.PairRouting.Assignments line 695
  63. instance OAI.ThorpNine.Dense.Thorp.PairRouting.(instance at line 698) line 698
  64. def OAI.ThorpNine.Dense.Thorp.PairRouting.routedEmbedding line 700
  65. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.occupied_pairLayer line 704
  66. def OAI.ThorpNine.Dense.Thorp.PairRouting.assignmentsEquiv line 707
  67. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.assignments_actual_bound line 716
  68. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.assignments_actual_exponent_nonneg line 724
  69. def OAI.ThorpNine.Dense.Thorp.PairRouting.compatibleSet line 734
  70. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.mem_compatibleSet line 739
  71. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.card_compatibleSet line 745
  72. def OAI.ThorpNine.Dense.Thorp.PairRouting.outerWeight line 750
  73. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.outerWeight_pos line 754
  74. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.sum_colors_factor line 759
  75. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.sandwich_weighted_probability line 774
  76. lemma OAI.ThorpNine.Dense.Thorp.PairRouting.tupleProbability_nonneg line 801