OAI/Probability/CubeShuffle/ModifiedRouting.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeShuffle.orbitSet_eq_of_agree line 9
2. def OAI.CubeShuffle.survivingCycle line 32
3. def OAI.CubeShuffle.perturbCycleMap line 41
4. lemma OAI.CubeShuffle.perturbCycleMap_injective line 49
5. theorem OAI.CubeShuffle.selectedCycle_perturb_le line 69

   Source documentation

   Changing a permutation on at most b specified inputs can destroy at most b of its wholly marked cycles. This is the exceptional-block loss in FAC.2.

   theorem selectedCycle_perturb_le (p q : Equiv.Perm α) (S B : Finset α)
       (h : ∀ x ∉ B, p x = q x) :
       Fintype.card (RoutingNetwork.SelectedCycle p S) ≤
         Fintype.card (RoutingNetwork.SelectedCycle q S)+B.card := by
   …

   Mentions: OAI.CubeShuffle.RoutingNetwork.SelectedCycle

6. def OAI.CubeShuffle.permDistance line 82
7. lemma OAI.CubeShuffle.permDistance_sum line 85
8. lemma OAI.CubeShuffle.permDistance_refl line 90
9. lemma OAI.CubeShuffle.permDistance_le line 93
10. lemma OAI.CubeShuffle.permDistance_symm line 96
11. lemma OAI.CubeShuffle.permDistance_triangle line 99
12. lemma OAI.CubeShuffle.permDistance_mul_left line 109
13. lemma OAI.CubeShuffle.permDistance_mul_right line 118
14. lemma OAI.CubeShuffle.permDistance_inv line 124
15. lemma OAI.CubeShuffle.permDistance_mul_le line 131
16. lemma OAI.CubeShuffle.selectedCycle_distance_le line 136
17. lemma OAI.CubeShuffle.permDistance_alternating line 143
18. lemma OAI.CubeShuffle.alternatingCycles_distance_le line 149
19. def OAI.CubeShuffle.centralBlockPerm line 169

    Source documentation

    An arbitrary independent permutation on each fixed central size-2^L block.

    def centralBlockPerm (L : ℕ) : (r : ℕ) → (Card r → Equiv.Perm (Card L)) →
        Equiv.Perm (Card (L+r))
      | 0, C => C (fun j => Fin.elim0 j)
      | r+1, C => childLift (fun b => centralBlockPerm L r (fun u => C (Fin.cons b u)))
    
    /-- A genuine palindrome with a specified permutation inserted in each central
    block. Fair coins below that boundary will later be absorbed or cancelled. -/

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.childLift

20. def OAI.CubeShuffle.centralPalindromePerm line 176

    Source documentation

    A genuine palindrome with a specified permutation inserted in each central block. Fair coins below that boundary will later be absorbed or cancelled.

    def centralPalindromePerm (L r : ℕ) (C : Card r → Equiv.Perm (Card L))
        (ω : BenesCoins (L+r)) : Equiv.Perm (Card (L+r)) :=
    …

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

21. lemma OAI.CubeShuffle.centralPalindromePerm_step line 181
22. def OAI.CubeShuffle.centralLevelCost line 202

    Source documentation

    The actual alternating cycles at one expanded height, with the central permutations left arbitrary. No low-level cycles are counted.

    noncomputable def centralLevelCost (t L : ℕ) : (r : ℕ) →
        (Card r → Equiv.Perm (Card L)) → {ι : Type*} → [Fintype ι] →
        (ι ↪ Card (L+r)) → BenesCoins (L+r) → ℕ
      | 0, _, _, _, _, _ => 0
      | r+1, C, _, _, e, ω =>
        let σ := benesStepEquiv (L+r) ω
    …

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

23. def OAI.CubeShuffle.centralSlabCost line 218
24. lemma OAI.CubeShuffle.permDistance_childLift line 222
25. def OAI.CubeShuffle.centralDistance line 246
26. lemma OAI.CubeShuffle.centralDistance_step line 249
27. lemma OAI.CubeShuffle.permDistance_centralBlock line 264
28. lemma OAI.CubeShuffle.permDistance_centralPalindrome line 273
29. lemma OAI.CubeShuffle.centralLevelCost_step line 280
30. lemma OAI.CubeShuffle.centralLevelCost_perturb line 297
31. lemma OAI.CubeShuffle.centralSlabCost_perturb line 327
32. lemma OAI.CubeShuffle.centralDistance_exceptional line 335
33. inductive OAI.CubeShuffle.InputTree line 353

    Source documentation

    A recursively paired input routing that may stop at any central block. The leaf maps are genuine permutations, not probabilistic hypotheses.

    inductive InputTree : ℕ → Type
      | tip {d : ℕ} (p : Equiv.Perm (Card d)) : InputTree d
      | node {d : ℕ} (ξ : Card d → Bool) (T : Bool → InputTree d) : InputTree (d+1)

    Mentions: OAI.CubeShuffle.Card

34. def OAI.CubeShuffle.InputTree.perm line 357
35. def OAI.CubeShuffle.InputTree.levelCost line 361
36. lemma OAI.CubeShuffle.InputTree.levelCost_node line 375
37. lemma OAI.CubeShuffle.InputTree.levelCost_gt line 390
38. lemma OAI.CubeShuffle.InputTree.levelCost_adapted line 398
39. theorem OAI.CubeShuffle.InputTree.level_partial_mgf line 431

    Source documentation

    The same fresh-layer bound is valid with arbitrary fixed central input maps. This is needed for, and preserves, the exceptional-block construction.

    theorem InputTree.level_partial_mgf (r s u : ℕ) (hu : u < r)
        (T : InputTree (s+r)) {ι : Type*} [Fintype ι] (e : ι ↪ Card (s+r))
        (lo : Card r × SwitchIndex s → Bool) (J : ℕ) (hJ : 0 < J) (q : ℝ) (hq : 1 ≤ q) :
        finiteMean (fun hi : Card s × SwitchIndex r → Bool =>
          q^(T.levelCost (s+u+1) e (assembleBits r s lo hi))) ≤
          Real.exp (Fintype.card ι * cycleCoefficient u J q) := by
    …

    Mentions: OAI.CubeShuffle.InputTree, OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.assembleBits, OAI.CubeShuffle.cycleCoefficient

40. def OAI.CubeShuffle.InputTree.slabCost line 510

    Source documentation

    Sum over a slab, padded by its actual zero costs when its levels exceed d.

    noncomputable def InputTree.slabCost (l d : ℕ) (T : InputTree d) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (Y : SwitchIndex d → Bool) : ℕ :=
    …

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

41. lemma OAI.CubeShuffle.InputTree.slabCost_adapted line 514
42. theorem OAI.CubeShuffle.InputTree.slab_partial_mgf line 523

    Source documentation

    The genuine conditional slab estimate: no independence is asserted among node cycles or among levels in the slab. Jensen costs l on the exponent.

    theorem InputTree.slab_partial_mgf (r s l : ℕ) (hl : 0 < l) (hs : 2*s ≤ l) (T : InputTree (s+r))
        {ι : Type*} [Fintype ι] (e : ι ↪ Card (s+r))
        (lo : Card r × SwitchIndex s → Bool) (q : ℝ) (hq : 1 ≤ q)
        (hlog : Real.log q ≤ 1/250) :
        finiteMean (fun hi : Card s × SwitchIndex r → Bool =>
          q^(InputTree.slabCost l (s+r) T e (assembleBits r s lo hi))) ≤
          Real.exp (Fintype.card ι * (68*Real.exp (-(l:ℝ)/64))) := by
    …

    Mentions: OAI.CubeShuffle.InputTree, OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.InputTree.slabCost, OAI.CubeShuffle.assembleBits

43. def OAI.CubeShuffle.boundaryTree line 573

    Source documentation

    A fixed central map in every block, with the genuine input-side fair layers above the boundary. The coins below L are ignored on this side.

    def boundaryTree (L : ℕ) : (r : ℕ) → (Card r → Equiv.Perm (Card L)) →
        (SwitchIndex (L+r) → Bool) → InputTree (L+r)
      | 0, U, _ => .tip (U (fun j => Fin.elim0 j))
      | r+1, U, X => .node (coinStepEquiv (L+r) X).2 (fun b =>
          boundaryTree L r (fun u => U (Fin.cons b u))
            (if b then (coinStepEquiv (L+r) X).1.2 else (coinStepEquiv (L+r) X).1.1))
    
    /-- The actual output butterfly in one central block. -/

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

44. def OAI.CubeShuffle.boundaryOutput line 581

    Source documentation

    The actual output butterfly in one central block.

    def boundaryOutput (L : ℕ) : (r : ℕ) → (SwitchIndex (L+r) → Bool) →
        Card r → Equiv.Perm (Card L)
      | 0, Y, _ => butterflyPerm L (decodeButterfly L Y)
      | r+1, Y, u => boundaryOutput L r
          (if u 0 then (coinStepEquiv (L+r) Y).1.2 else (coinStepEquiv (L+r) Y).1.1) (Fin.tail u)

    Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.Card, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.coinStepEquiv

45. lemma OAI.CubeShuffle.boundaryOutput_adapted line 587
46. def OAI.CubeShuffle.modifiedBoundary line 604

    Source documentation

    In an exceptional block the input map equals its output map, so the central permutation is exactly identity. Elsewhere its inverse is uniform.

    noncomputable def modifiedBoundary (L r : ℕ) (E : Finset (Card r))
        (U : Card r → Equiv.Perm (Card L)) (Y : SwitchIndex (L+r) → Bool) :
        Card r → Equiv.Perm (Card L) := fun u => if u ∈ E then boundaryOutput L r Y u else U u

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

47. lemma OAI.CubeShuffle.modifiedBoundary_adapted line 608
48. lemma OAI.CubeShuffle.permDistance_boundaryTree line 615
49. lemma OAI.CubeShuffle.boundaryTree_levelCost_perturb line 627
50. lemma OAI.CubeShuffle.boundaryTree_slabCost_perturb line 665
51. lemma OAI.CubeShuffle.modifiedBoundary_distance_le line 675
52. lemma OAI.CubeShuffle.InputTree.slabCost_gt line 685
53. lemma OAI.CubeShuffle.InputTree.random_slab_adapted_mul_le line 692
54. lemma OAI.CubeShuffle.InputTree.slab_mgf line 709
55. def OAI.CubeShuffle.InputTree.familyCost line 719
56. lemma OAI.CubeShuffle.InputTree.random_slabCost_adapted line 724
57. lemma OAI.CubeShuffle.InputTree.familyCost_adapted line 733
58. theorem OAI.CubeShuffle.InputTree.family_mgf_first line 743

    Source documentation

    Only the first slab pays for the exceptional central maps. Later slabs condition on them, using independent outward layers, exactly as FAC.2.

    theorem InputTree.family_mgf_first (L n d s : ℕ) (hL : 0 < L) (hs : s ≤ L)
        (T : (SwitchIndex d → Bool) → InputTree d) (hT : LayerAdapted d s T)
        {ι : Type*} [Fintype ι] (e : ι ↪ Card d) (q : ℝ) (hq : 1 ≤ q)
        (hlog : Real.log q ≤ 1/250) (p : ℝ) (hp : 0 ≤ p)
        (hfirst : finiteMean (fun Y => q^(InputTree.slabCost L d (T Y) e Y)) ≤
          Real.exp (p+Fintype.card ι*(68*Real.exp (-(L:ℝ)/64)))) :
        finiteMean (fun Y => q^(InputTree.familyCost L n d T e Y)) ≤
          Real.exp (p+Fintype.card ι*(68*∑ j ∈ Finset.range n,
            Real.exp (-((L*4^j:ℕ):ℝ)/64))) := by
    …

    Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.InputTree, OAI.CubeShuffle.LayerAdapted, OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.InputTree.slabCost, OAI.CubeShuffle.InputTree.familyCost

59. lemma OAI.CubeShuffle.InputTree.family_mgf_first_decay line 793
60. def OAI.CubeShuffle.modifiedInputTree line 811
61. lemma OAI.CubeShuffle.modifiedInputTree_adapted line 815
62. lemma OAI.CubeShuffle.modified_slab_mgf line 822
63. lemma OAI.CubeShuffle.modified_family_mgf line 848
64. theorem OAI.CubeShuffle.modified_high_mgf line 861

    Source documentation

    The actual exceptional-block high-level moment: the exceptional loss is paid in the first slab of each family only, not at every height.

    theorem modified_high_mgf (L n r : ℕ) (hL : 0 < L) (E : Finset (Card r))
        (U : Card r → Equiv.Perm (Card L)) (X : SwitchIndex (L+r) → Bool)
        {ι : Type*} [Fintype ι] (e : ι ↪ Card (L+r)) (q : ℝ) (hq : 1 ≤ q)
        (hlog : Real.log q ≤ 1/500) :
        finiteMean (fun Y => q^(InputTree.familyCost L n (L+r) (modifiedInputTree L r E U X) e Y+
          InputTree.familyCost (2*L) n (L+r) (modifiedInputTree L r E U X) e Y)) ≤
          Real.exp (Fintype.card ι*heightDecay L +
            3*((L*E.card*2^L:ℕ):ℝ)*Real.log q) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.InputTree.familyCost, OAI.CubeShuffle.modifiedInputTree, OAI.CubeShuffle.heightDecay

65. def OAI.CubeShuffle.InputTree.lowCost line 890
66. lemma OAI.CubeShuffle.InputTree.lowCost_slab line 894
67. lemma OAI.CubeShuffle.InputTree.cost_family line 901
68. lemma OAI.CubeShuffle.InputTree.lowCost_ge line 915
69. lemma OAI.CubeShuffle.boundaryTree_levelCost_low line 924
70. lemma OAI.CubeShuffle.boundaryTree_lowCost_zero line 933
71. theorem OAI.CubeShuffle.modified_cost_mgf line 943

    Source documentation

    Quantitative FAC.2 cycle moment, with fixed outer input layers and fixed independent uniform central seeds. The latter may now be averaged freely.

    theorem modified_cost_mgf (L r : ℕ) (hL : 0 < L) (E : Finset (Card r))
        (U : Card r → Equiv.Perm (Card L)) (X : SwitchIndex (L+r) → Bool)
        {ι : Type*} [Fintype ι] (e : ι ↪ Card (L+r)) (q : ℝ) (hq : 1 ≤ q)
        (hlog : Real.log q ≤ 1/500) :
        finiteMean (fun Y => q^(InputTree.lowCost (L+r) (L+r) (modifiedInputTree L r E U X Y) e Y)) ≤
          Real.exp (Fintype.card ι*heightDecay L +
            3*((L*E.card*2^L:ℕ):ℝ)*Real.log q) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.InputTree.lowCost, OAI.CubeShuffle.modifiedInputTree, OAI.CubeShuffle.heightDecay