OAI/Probability/CubeShuffle/ParallelLayers.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.parallelPerm line 13
2. def OAI.CubeShuffle.relabeledPerm line 19
3. def OAI.CubeShuffle.parallelPath line 23
4. def OAI.CubeShuffle.parallelUsers line 29
5. lemma OAI.CubeShuffle.parallelUsers_ne line 35
6. lemma OAI.CubeShuffle.mem_parallelPath line 41
7. lemma OAI.CubeShuffle.card_parallelPath line 74
8. def OAI.CubeShuffle.blockMarks line 79
9. lemma OAI.CubeShuffle.mem_blockMarks line 83
10. lemma OAI.CubeShuffle.sum_card_blockMarks line 89
11. lemma OAI.CubeShuffle.card_blockMarks_le line 100
12. lemma OAI.CubeShuffle.parallel_entropy line 106
13. def OAI.CubeShuffle.parallelFollow line 129
14. lemma OAI.CubeShuffle.parallelFollow_succeeds line 134
15. lemma OAI.CubeShuffle.parallelFollow_raw_charge line 140
16. lemma OAI.CubeShuffle.parallelFollow_stale_charge line 146
17. def OAI.CubeShuffle.closingDomain line 153
18. def OAI.CubeShuffle.closingValue line 157
19. lemma OAI.CubeShuffle.relabeled_endpoint_pair line 161
20. lemma OAI.CubeShuffle.relabeled_endpoint_iff line 170
21. lemma OAI.CubeShuffle.closingDomain_eq line 180
22. def OAI.CubeShuffle.parallelClose line 185
23. lemma OAI.CubeShuffle.parallelClose_succeeds line 192
24. lemma OAI.CubeShuffle.parallelClose_raw_charge line 204
25. lemma OAI.CubeShuffle.parallelClose_fresh_charge line 214
26. lemma OAI.CubeShuffle.parallelClose_stale_charge line 225
27. def OAI.CubeShuffle.parallelNetwork line 240

    Source documentation

    Independent fair butterflies in parallel with completely arbitrary fixed bijections at either end. All certificate fields are proved from the explicit Boolean query algorithms and deterministic butterfly geometry.

    noncomputable def parallelNetwork (pre : α ≃ B × Card d) (post : B × Card d ≃ α) :
        RoutingNetwork α (B × SwitchIndex d) d where
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.RoutingNetwork, OAI.CubeShuffle.SwitchIndex

28. lemma OAI.CubeShuffle.parallel_cycle_log_mgf line 260

    Source documentation

    The source FAC.4 estimate for independent parallel butterflies, allowing arbitrary fixed identifications on both sides.

    lemma parallel_cycle_log_mgf (pre : α ≃ B × Card d) (post : B × Card d ≃ α)
        (S : Finset α) (J : ℕ) (hJ : 0 < J) (q : ℝ) (hq : 1 ≤ q) :
        Real.log (finiteMean (fun ω : B × SwitchIndex d → Bool =>
          q^(Fintype.card (RoutingNetwork.SelectedCycle (relabeledPerm pre post ω) S)))) ≤
          (S.card : ℝ)/J * Real.log q + 2*q*S.card*Real.sqrt J / Real.sqrt ((2:ℝ)^d) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.RoutingNetwork.SelectedCycle, OAI.CubeShuffle.relabeledPerm

29. def OAI.CubeShuffle.cardSplit line 272

    Source documentation

    Separate the first r coordinates from the remaining s coordinates. The sum is written s+r so its recursion agrees literally with the network.

    def cardSplit : (r s : ℕ) → Card (s+r) ≃ Card r × Card s
      | 0, s =>
        { toFun := fun x => ((fun i => Fin.elim0 i), x)
    …

    Mentions: OAI.CubeShuffle.Card

30. def OAI.CubeShuffle.assembleBits line 294

    Source documentation

    Assemble the previously exposed low layers and the still-fresh high layers without identifying or resampling any switch coin.

    def assembleBits : (r s : ℕ) → (Card r × SwitchIndex s → Bool) →
        (Card s × SwitchIndex r → Bool) → SwitchIndex (s+r) → Bool
      | 0, _, lo, _, i => lo ((fun j => Fin.elim0 j), i)
      | r+1, s, _, hi, Sum.inl y => hi ((cardSplit r s y).2,Sum.inl (cardSplit r s y).1)
      | r+1, s, lo, hi, Sum.inr (b,i) => assembleBits r s
          (fun j => lo (Fin.cons b j.1,j.2)) (fun j => hi (j.1,Sum.inr (b,j.2))) i

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.cardSplit

31. lemma OAI.CubeShuffle.butterfly_split line 301
32. def OAI.CubeShuffle.splitSwitch line 329

    Source documentation

    Disjoint partition of all switch locations into the exposed low butterflies and the remaining high butterflies.

    def splitSwitch : (r s : ℕ) → SwitchIndex (s+r) ≃
        (Card r × SwitchIndex s) ⊕ (Card s × SwitchIndex r)
      | 0, _ =>
        { toFun := fun i => Sum.inl ((fun j => Fin.elim0 j),i)
    …

    Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.Card

33. lemma OAI.CubeShuffle.assembleBits_eq line 373
34. def OAI.CubeShuffle.splitCoinEquiv line 387

    Source documentation

    The actual uniform coin law splits as a product; this is an equivalence of finite sample spaces, rather than an independence assumption.

    def splitCoinEquiv (r s : ℕ) :
        ((Card r × SwitchIndex s → Bool) × (Card s × SwitchIndex r → Bool)) ≃
          (SwitchIndex (s+r) → Bool) :=
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex

35. lemma OAI.CubeShuffle.splitCoinEquiv_apply line 393
36. lemma OAI.CubeShuffle.finiteMean_prod line 399
37. lemma OAI.CubeShuffle.finiteMean_split line 404
38. def OAI.CubeShuffle.freshPre line 419
39. def OAI.CubeShuffle.freshPost line 423
40. lemma OAI.CubeShuffle.exposed_perm_eq line 426
41. lemma OAI.CubeShuffle.partially_exposed_cycle_log_mgf line 437

    Source documentation

    Single-level FAC.4 after any fixed exposure of the first s outward layers. The expectation is over the genuinely unexposed disjoint high-layer coins.

    lemma partially_exposed_cycle_log_mgf [Fintype α] [DecidableEq α]
        (pre : α ≃ Card (s+r)) (post : Card (s+r) ≃ α)
        (lo : Card r × SwitchIndex s → Bool) (S : Finset α)
        (J : ℕ) (hJ : 0 < J) (q : ℝ) (hq : 1 ≤ q) :
        Real.log (finiteMean (fun hi : Card s × SwitchIndex r → Bool =>
          q^(Fintype.card (RoutingNetwork.SelectedCycle
            ((pre.trans (butterflyPerm (s+r)
              (decodeButterfly (s+r) (assembleBits r s lo hi)))).trans post) S)))) ≤
          (S.card : ℝ)/J * Real.log q + 2*q*S.card*Real.sqrt J / Real.sqrt ((2:ℝ)^r) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.RoutingNetwork.SelectedCycle, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.assembleBits

42. lemma OAI.CubeShuffle.inclusionMoment_eq line 451
43. lemma OAI.CubeShuffle.finiteMean_bool line 459
44. lemma OAI.CubeShuffle.finiteMean_const line 463
45. lemma OAI.CubeShuffle.finiteMean_pi_prod line 468
46. def OAI.CubeShuffle.pairLayer line 476
47. def OAI.CubeShuffle.pairFiber line 488
48. lemma OAI.CubeShuffle.prod_pairFiber line 491
49. lemma OAI.CubeShuffle.fiber_average_bound line 501
50. lemma OAI.CubeShuffle.CylinderBound.fair_parallel line 514

    Source documentation

    A whole layer of independent fair pair coins preserves the upper-product bound. Dependence in the random marked set is not discarded.

    lemma CylinderBound.fair_parallel {m : Finset (Bool × β) → ℝ} {p : Bool × β → ℝ}
        (h : CylinderBound m p) (hp : ∀ x, 0 ≤ p x) :
        CylinderBound (fun S => finiteMean (fun ξ : β → Bool => m (S.image (pairLayer ξ))))
          (fun x => (p x+p (!x.1,x.2))/2) := by
    …

    Mentions: OAI.CubeShuffle.CylinderBound, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.pairLayer

51. lemma OAI.CubeShuffle.subset_pairLayer_image_iff line 540
52. def OAI.CubeShuffle.fairSetLayer line 551
53. lemma OAI.CubeShuffle.finiteMean_comm line 554
54. lemma OAI.CubeShuffle.inclusionMoment_fairSetLayer line 559
55. lemma OAI.CubeShuffle.inclusionMoment_fairSetLayer_singleton line 574
56. lemma OAI.CubeShuffle.cylinder_fairSetLayer line 585
57. lemma OAI.CubeShuffle.subset_image_equiv_iff line 602
58. lemma OAI.CubeShuffle.inclusionMoment_image_equiv line 613
59. lemma OAI.CubeShuffle.cylinder_image_equiv line 622
60. lemma OAI.CubeShuffle.inclusionMoment_comp_equiv line 632
61. lemma OAI.CubeShuffle.cylinder_comp_equiv line 640
62. lemma OAI.CubeShuffle.finiteMean_prod_mul line 648
63. def OAI.CubeShuffle.childJoin line 658
64. lemma OAI.CubeShuffle.mem_childJoin line 661
65. def OAI.CubeShuffle.boolFiber line 665
66. lemma OAI.CubeShuffle.mem_boolFiber line 668
67. lemma OAI.CubeShuffle.childJoin_boolFiber line 680
68. lemma OAI.CubeShuffle.subset_childJoin_iff line 686
69. lemma OAI.CubeShuffle.prod_childJoin line 701
70. lemma OAI.CubeShuffle.prod_boolFibers line 714
71. lemma OAI.CubeShuffle.inclusionMoment_childJoin line 719
72. lemma OAI.CubeShuffle.cylinder_childJoin line 731
73. def OAI.CubeShuffle.coinStepEquiv line 763

    Source documentation

    Exact independent split of a butterfly's last layer and its two children.

    def coinStepEquiv (d : ℕ) : (SwitchIndex (d+1) → Bool) ≃
        ((SwitchIndex d → Bool) × (SwitchIndex d → Bool)) × (Card d → Bool) where
    …

    Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.Card

74. def OAI.CubeShuffle.headTailEquiv line 777
75. lemma OAI.CubeShuffle.childMarks_join line 780
76. def OAI.CubeShuffle.butterflyMarks line 801
77. lemma OAI.CubeShuffle.butterflyMarks_succ line 805
78. lemma OAI.CubeShuffle.butterflyMarks_cylinder line 834

    Source documentation

    The actual central marked positions obey the product-of-marginals upper bound, not just an independently resampled proxy.

    lemma butterflyMarks_cylinder (d : ℕ) (A : Finset (Card d)) :
        CylinderBound (inclusionMoment (butterflyMarks d A))
          (fun x => inclusionMoment (butterflyMarks d A) {x}) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.CylinderBound, OAI.CubeShuffle.inclusionMoment, OAI.CubeShuffle.butterflyMarks

79. lemma OAI.CubeShuffle.indicator_mem_image_perm line 851
80. lemma OAI.CubeShuffle.butterflyMarks_singleton line 870
81. lemma OAI.CubeShuffle.butterflyMarks_inclusion line 880

    Source documentation

    The joint inclusion bound used for the low levels of FAC.1.

    lemma butterflyMarks_inclusion (d : ℕ) (A S : Finset (Card d)) :
        inclusionMoment (butterflyMarks d A) S ≤ ((A.card : ℝ)/(2:ℝ)^d)^S.card := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.inclusionMoment, OAI.CubeShuffle.butterflyMarks