OAI/Probability/CubeShuffle/PairRouting.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.PairRouting.occupied line 13
2. lemma OAI.CubeShuffle.PairRouting.mem_occupied line 17
3. def OAI.CubeShuffle.PairRouting.required line 20
4. def OAI.CubeShuffle.PairRouting.Compatible line 22
5. def OAI.CubeShuffle.PairRouting.colors line 25
6. lemma OAI.CubeShuffle.PairRouting.required_colors line 29
7. lemma OAI.CubeShuffle.PairRouting.colors_compatible line 35
8. def OAI.CubeShuffle.PairRouting.chosenCoin line 39
9. lemma OAI.CubeShuffle.PairRouting.chosenCoin_apply line 44
10. lemma OAI.CubeShuffle.PairRouting.colors_eq_iff line 51
11. instance OAI.CubeShuffle.PairRouting.(instance at line 63) line 63
12. lemma OAI.CubeShuffle.PairRouting.colors_probability line 68

    Source documentation

    Exact fair-coin probability at an outer pair layer, including impossible assignments. No cardinality or independence of marked paths is assumed.

    lemma colors_probability (x : ι → Bool × α) (c : ι → Bool) :
        finiteMean (fun ξ : α → Bool => if colors x ξ = c then (1 : ℝ) else 0) =
          if Compatible x c then 1/(2:ℝ)^(occupied x).card else 0 := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.PairRouting.colors, OAI.CubeShuffle.PairRouting.Compatible, OAI.CubeShuffle.PairRouting.occupied

13. lemma OAI.CubeShuffle.PairRouting.Compatible.tail_injective line 82
14. def OAI.CubeShuffle.PairRouting.childEmbedding line 93
15. def OAI.CubeShuffle.PairRouting.lift line 101
16. def OAI.CubeShuffle.PairRouting.sandwich line 107
17. def OAI.CubeShuffle.PairRouting.ChildMatches line 110
18. instance OAI.CubeShuffle.PairRouting.(instance at line 113) line 113
19. lemma OAI.CubeShuffle.PairRouting.sandwich_matches_iff line 117
20. lemma OAI.CubeShuffle.PairRouting.sandwich_probability line 130

    Source documentation

    Exact expansion by the binary child assignments at one actual outer pair layer on each side. The factors 2^-b count occupied switches, not paths.

    lemma sandwich_probability [DecidableEq ι] (p : Bool → Equiv.Perm α) (x y : ι → Bool × α) :
        finiteMean (fun coins : (α → Bool) × (α → Bool) =>
          if ∀ i, sandwich coins.1 coins.2 p (x i) = y i then (1:ℝ) else 0) =
        ∑ c : ι → Bool,
          (if Compatible x c then 1/(2:ℝ)^(occupied x).card else 0) *
          (if Compatible y c then 1/(2:ℝ)^(occupied y).card else 0) *
          (if ChildMatches p x y c then 1 else 0) := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.PairRouting.sandwich, OAI.CubeShuffle.PairRouting.Compatible, OAI.CubeShuffle.PairRouting.occupied, OAI.CubeShuffle.PairRouting.ChildMatches

21. lemma OAI.CubeShuffle.PairRouting.childMatches_split line 160
22. def OAI.CubeShuffle.PairRouting.tupleProbability line 176
23. lemma OAI.CubeShuffle.PairRouting.childMatches_mean line 182
24. lemma OAI.CubeShuffle.PairRouting.sandwich_mean line 201

    Source documentation

    The exact recursive transition identity before taking any moment bound.

    lemma sandwich_mean [DecidableEq ι] {Ω Ω' : Type*} [Fintype Ω] [Fintype Ω']
        (P : Ω → Equiv.Perm α) (Q : Ω' → Equiv.Perm α) (x y : ι → Bool × α) :
        finiteMean (fun ω : Ω × Ω' => finiteMean (fun coins : (α → Bool) × (α → Bool) =>
          if ∀ i, sandwich coins.1 coins.2 (fun b => if b then Q ω.2 else P ω.1) (x i) = y i
          then (1:ℝ) else 0)) =
        ∑ c : ι → Bool,
          (if Compatible x c then 1/(2:ℝ)^(occupied x).card else 0) *
          (if Compatible y c then 1/(2:ℝ)^(occupied y).card else 0) *
          (tupleProbability P (fun i : {i // c i = false} => (x i.val).2)
            (fun i : {i // c i = false} => (y i.val).2) *
          tupleProbability Q (fun i : {i // c i = true} => (x i.val).2)
            (fun i : {i // c i = true} => (y i.val).2)) := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.PairRouting.sandwich, OAI.CubeShuffle.PairRouting.Compatible, OAI.CubeShuffle.PairRouting.occupied, OAI.CubeShuffle.PairRouting.tupleProbability

25. abbrev OAI.CubeShuffle.PairRouting.BothAssignments line 226
26. instance OAI.CubeShuffle.PairRouting.(instance at line 229) line 229
27. def OAI.CubeShuffle.PairRouting.labelSet line 232
28. def OAI.CubeShuffle.PairRouting.alternatingProjection line 234
29. def OAI.CubeShuffle.PairRouting.assignmentColoring line 236
30. lemma OAI.CubeShuffle.PairRouting.assignmentColoring_injective line 275
31. lemma OAI.CubeShuffle.PairRouting.bothAssignments_card line 285
32. lemma OAI.CubeShuffle.PairRouting.occupied_labelSet line 298
33. lemma OAI.CubeShuffle.PairRouting.image_snd_childJoin line 303
34. lemma OAI.CubeShuffle.PairRouting.image_lift_childJoin line 308
35. lemma OAI.CubeShuffle.PairRouting.occupied_lift_card line 314
36. lemma OAI.CubeShuffle.PairRouting.bothAssignments_occupied_bound line 331
37. lemma OAI.CubeShuffle.PairRouting.compatible_pairLayer_iff line 345
38. def OAI.CubeShuffle.PairRouting.alternatingCycles line 366

    Source documentation

    Full alternating cycles, not their projection-side overcount. This is the cycle count needed for sparse low-level blocks.

    noncomputable def alternatingCycles (e : ι ↪ Bool × α) (p : Bool → Equiv.Perm α) : ℕ :=
    …

39. lemma OAI.CubeShuffle.PairRouting.occupied_eq_fibers line 371
40. lemma OAI.CubeShuffle.PairRouting.card_labelSet line 377
41. lemma OAI.CubeShuffle.PairRouting.occupied_card_double line 382
42. lemma OAI.CubeShuffle.PairRouting.bothAssignments_exact_bound line 393
43. abbrev OAI.CubeShuffle.PairRouting.Assignments line 413
44. instance OAI.CubeShuffle.PairRouting.(instance at line 416) line 416
45. def OAI.CubeShuffle.PairRouting.switchedEmbedding line 418
46. def OAI.CubeShuffle.PairRouting.routedEmbedding line 421
47. lemma OAI.CubeShuffle.PairRouting.occupied_pairLayer line 425
48. def OAI.CubeShuffle.PairRouting.assignmentsEquiv line 428
49. lemma OAI.CubeShuffle.PairRouting.assignments_actual_bound line 437
50. lemma OAI.CubeShuffle.PairRouting.assignments_actual_exponent_nonneg line 445
51. def OAI.CubeShuffle.PairRouting.compatibleSet line 457
52. lemma OAI.CubeShuffle.PairRouting.mem_compatibleSet line 462
53. lemma OAI.CubeShuffle.PairRouting.card_compatibleSet line 468
54. def OAI.CubeShuffle.PairRouting.outerWeight line 473
55. lemma OAI.CubeShuffle.PairRouting.outerWeight_pos line 477
56. lemma OAI.CubeShuffle.PairRouting.sum_colors_factor line 482
57. lemma OAI.CubeShuffle.PairRouting.sandwich_weighted_probability line 499

    Source documentation

    Arbitrary weights can be kept as functions of the actual child assignment; no change from the physical switch measure to uniformly sampled assignments.

    lemma sandwich_weighted_probability (p : Bool → Equiv.Perm α) (x y : ι → Bool × α)
        (W : (ι → Bool) → ℝ) :
        finiteMean (fun coins : (α → Bool) × (α → Bool) =>
          if ∀ i, sandwich coins.1 coins.2 p (x i) = y i then W (colors x coins.1) else 0) =
        outerWeight x y * ∑ c ∈ compatibleSet x y, if ChildMatches p x y c then W c else 0 := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.PairRouting.sandwich, OAI.CubeShuffle.PairRouting.colors, OAI.CubeShuffle.PairRouting.outerWeight, OAI.CubeShuffle.PairRouting.compatibleSet, OAI.CubeShuffle.PairRouting.ChildMatches

58. lemma OAI.CubeShuffle.PairRouting.tupleProbability_nonneg line 526
59. lemma OAI.CubeShuffle.PairRouting.sandwich_power_bound line 532

    Source documentation

    One precise Hölder step in the source recursive density expansion.

    lemma sandwich_power_bound {Ω Ω' : Type*} [Fintype Ω] [Fintype Ω']
        (P : Ω → Equiv.Perm α) (Q : Ω' → Equiv.Perm α) (x y : ι → Bool × α)
        (a : ℝ) (ha : 0 ≤ a) :
        (finiteMean (fun ω : Ω × Ω' => finiteMean (fun coins : (α → Bool) × (α → Bool) =>
          if ∀ i, sandwich coins.1 coins.2 (fun b => if b then Q ω.2 else P ω.1) (x i) = y i
          then (1:ℝ) else 0)))^(1+a) ≤
        (outerWeight x y)^(1+a) * ((compatibleSet x y).card:ℝ)^a *
          ∑ c ∈ compatibleSet x y,
          (tupleProbability P (fun i : {i // c i = false} => (x i.val).2)
            (fun i : {i // c i = false} => (y i.val).2))^(1+a) *
          (tupleProbability Q (fun i : {i // c i = true} => (x i.val).2)
            (fun i : {i // c i = true} => (y i.val).2))^(1+a) := by
    …

    Mentions: OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.PairRouting.sandwich, OAI.CubeShuffle.PairRouting.outerWeight, OAI.CubeShuffle.PairRouting.compatibleSet, OAI.CubeShuffle.PairRouting.tupleProbability

60. abbrev OAI.CubeShuffle.BenesCoins line 573

    Source documentation

    Two genuine independent butterfly coin fields; the first routes outward on the output side, the second outward on the input side.

    abbrev BenesCoins (d : ℕ) := (SwitchIndex d → Bool) × (SwitchIndex d → Bool)

    Mentions: OAI.CubeShuffle.SwitchIndex

61. def OAI.CubeShuffle.palindromePerm line 575
62. def OAI.CubeShuffle.sandwichShuffle line 579

    Source documentation

    Exact rearrangement, not a resampling assumption.

    def sandwichShuffle {A B C D E F : Type*} :
        ((A × B) × C) × ((D × E) × F) ≃ ((A × D) × (B × E)) × (F × C) where
    …

63. def OAI.CubeShuffle.benesStepEquiv line 586
64. lemma OAI.CubeShuffle.childLift_mul line 590
65. lemma OAI.CubeShuffle.childLift_inv line 595
66. lemma OAI.CubeShuffle.pairSwitch_inv line 598
67. lemma OAI.CubeShuffle.palindromePerm_step line 600
68. lemma OAI.CubeShuffle.headTail_switch line 616
69. lemma OAI.CubeShuffle.headTail_child line 619
70. lemma OAI.CubeShuffle.palindromePerm_coordinates line 623

    Source documentation

    The complete actual recursive Beneš construction in product coordinates.

    lemma palindromePerm_coordinates (d : ℕ) (c : BenesCoins d × BenesCoins d)
        (coins : (Card d → Bool) × (Card d → Bool)) (x : Card (d+1)) :
        headTailEquiv d (palindromePerm (d+1) ((benesStepEquiv d).symm (c,coins)) x) =
          PairRouting.sandwich coins.1 coins.2 (fun b => palindromePerm d (if b then c.2 else c.1))
            (headTailEquiv d x) := by
    …

    Mentions: OAI.CubeShuffle.BenesCoins, OAI.CubeShuffle.Card, OAI.CubeShuffle.headTailEquiv, OAI.CubeShuffle.palindromePerm, OAI.CubeShuffle.benesStepEquiv, OAI.CubeShuffle.PairRouting.sandwich

71. def OAI.CubeShuffle.palindromeCost line 634

    Source documentation

    Full alternating-cycle count along the ACTUAL sampled routing, recursively. At each child the labels are exactly those sent into it by the actual input coins.

    noncomputable def palindromeCost : (d : ℕ) → {ι : Type*} → [Fintype ι] →
        (ι ↪ Card d) → BenesCoins d → ℕ
      | 0, _, _, _, _ => 0
      | d+1, _, _, e, ω =>
          let σ := benesStepEquiv d ω
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.BenesCoins, OAI.CubeShuffle.benesStepEquiv

72. lemma OAI.CubeShuffle.CycleColoring.alternating_cycle_two line 650
73. lemma OAI.CubeShuffle.CycleColoring.alternating_cycle_count_double line 668
74. lemma OAI.CubeShuffle.CycleColoring.alternating_cycle_count_zero line 677
75. lemma OAI.CubeShuffle.PairRouting.alternatingCycles_double line 687
76. lemma OAI.CubeShuffle.PairRouting.alternatingCycles_zero line 692
77. lemma OAI.CubeShuffle.PairRouting.colors_chosenCoin line 703
78. def OAI.CubeShuffle.PairRouting.coloredEmbedding line 709
79. lemma OAI.CubeShuffle.PairRouting.coloredEmbedding_apply line 713
80. lemma OAI.CubeShuffle.PairRouting.switchedEmbedding_eq_colored line 720
81. lemma OAI.CubeShuffle.PairRouting.assignments_match_bound line 729
82. lemma OAI.CubeShuffle.PairRouting.occupied_sum_ge line 749
83. lemma OAI.CubeShuffle.PairRouting.assignment_weight_bound line 757

    Source documentation

    The exact cancellation giving the source factor 2^(-h+z), before taking its a-th power. Natural subtraction is justified by occupied-pair cardinalities.

    lemma assignment_weight_bound (x y : ι ↪ Bool × α) (c : ι → Bool)
        (hc : c ∈ compatibleSet x y) (p : Bool → Equiv.Perm α) (hm : ChildMatches p x y c) :
        ((compatibleSet x y).card:ℝ) * outerWeight x y ≤
          (2:ℝ)^((alternatingCycles
            (coloredEmbedding x c (mem_compatibleSet x y c |>.mp hc).1) p : ℝ) - Fintype.card ι) := by
    …

    Mentions: OAI.CubeShuffle.PairRouting.compatibleSet, OAI.CubeShuffle.PairRouting.ChildMatches, OAI.CubeShuffle.PairRouting.outerWeight, OAI.CubeShuffle.PairRouting.alternatingCycles, OAI.CubeShuffle.PairRouting.coloredEmbedding, OAI.CubeShuffle.PairRouting.mem_compatibleSet

84. lemma OAI.CubeShuffle.PairRouting.assignment_factor_bound line 778
85. lemma OAI.CubeShuffle.PairRouting.sandwich_weighted_probability_subtype line 795
86. lemma OAI.CubeShuffle.PairRouting.color_card_add line 806