OAI/Probability/CubeShuffle/DensityMoments.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.parallelFreshPre line 9
2. def OAI.CubeShuffle.parallelFreshPost line 16
3. def OAI.CubeShuffle.parallelAssembled line 20
4. lemma OAI.CubeShuffle.parallel_exposed_perm line 24
5. theorem OAI.CubeShuffle.parallel_partially_exposed_log_mgf line 40

   Source documentation

   Uniform conditional FAC.4 for an actual parallel network, after fixed exposure of every low layer and with arbitrary fixed endpoint relabelings.

   theorem parallel_partially_exposed_log_mgf [Fintype α] [DecidableEq α] [Fintype B] [DecidableEq B]
       (pre : α ≃ B × Card (s+r)) (post : B × Card (s+r) ≃ α)
       (lo : B → Card r × SwitchIndex s → Bool) (S : Finset α)
       (J : ℕ) (hJ : 0 < J) (q : ℝ) (hq : 1 ≤ q) :
       Real.log (finiteMean (fun hi : (B × Card s) × SwitchIndex r → Bool =>
         q^(Fintype.card (RoutingNetwork.SelectedCycle
           (relabeledPerm pre post (parallelAssembled lo hi)) 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.relabeledPerm, OAI.CubeShuffle.parallelAssembled

6. lemma OAI.CubeShuffle.orbitSet_inverse line 57
7. lemma OAI.CubeShuffle.selectedCycle_inverse line 61
8. lemma OAI.CubeShuffle.orbitSet_conjugate line 74
9. def OAI.CubeShuffle.conjugateCycle line 87
10. lemma OAI.CubeShuffle.conjugateCycle_injective line 94
11. lemma OAI.CubeShuffle.selectedCycle_conjugate line 100
12. lemma OAI.CubeShuffle.alternatingCycles_le_projection line 122
13. lemma OAI.CubeShuffle.projectionCycles_forward line 133

    Source documentation

    Cycle orientation is explicitly reversed after conjugating by the fixed input map. The remaining random zero-side map is a forward butterfly.

    lemma projectionCycles_forward (X₀ X₁ Y₀ Y₁ : Equiv.Perm α) (S : Finset α) :
        Fintype.card (RoutingNetwork.SelectedCycle
          ((Y₀*X₀⁻¹)⁻¹*(Y₁*X₁⁻¹)) S) =
        Fintype.card (RoutingNetwork.SelectedCycle
          (X₀⁻¹*X₁*Y₁⁻¹*Y₀) (S.image X₀.symm)) := by
    …

    Mentions: OAI.CubeShuffle.RoutingNetwork.SelectedCycle

14. def OAI.CubeShuffle.cycleCoefficient line 156
15. lemma OAI.CubeShuffle.cycleCoefficient_nonneg line 159
16. lemma OAI.CubeShuffle.projectionSide_card_le line 165
17. theorem OAI.CubeShuffle.node_partial_mgf line 174

    Source documentation

    Conditional moment for one actual pair-routing node. The input-side maps are fixed; only the unexposed zero-side output butterfly is averaged.

    theorem node_partial_mgf (r s : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Bool × Card (s+r)) (X₀ X₁ Y₁ : Equiv.Perm (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^(PairRouting.alternatingCycles e (fun b => if b then Y₁*X₁⁻¹ else
            butterflyPerm (s+r) (decodeButterfly (s+r) (assembleBits r s lo hi))*X₀⁻¹))) ≤
          Real.exp (Fintype.card ι * cycleCoefficient r J q) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.PairRouting.alternatingCycles, OAI.CubeShuffle.butterflyPerm, OAI.CubeShuffle.decodeButterfly, OAI.CubeShuffle.assembleBits, OAI.CubeShuffle.cycleCoefficient

18. def OAI.CubeShuffle.highStepEquiv line 222

    Source documentation

    Expose the last fresh layer, retaining the two independent lower fresh halves. This is a bijection of the original fair coin spaces.

    def highStepEquiv (r s : ℕ) : (Card s × SwitchIndex (r+1) → Bool) ≃
        (((Card s × SwitchIndex r → Bool) × (Card s × SwitchIndex r → Bool)) ×
          (Card s × Card r → Bool)) where
    …

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

19. lemma OAI.CubeShuffle.assembleBits_step line 239
20. def OAI.CubeShuffle.palindromeLevelCost line 254

    Source documentation

    The exact level cost in the actual palindrome recursion. It stops at the specified height, and sums across all independent child nodes.

    noncomputable def palindromeLevelCost (t : ℕ) : (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

21. lemma OAI.CubeShuffle.palindromeLevelCost_step line 267
22. lemma OAI.CubeShuffle.palindromeLevelCost_gt line 282
23. theorem OAI.CubeShuffle.palindrome_level_partial_mgf line 296

    Source documentation

    Uniform conditional FAC.4 for the actual sum of node cycles at one height. All input coins and all output layers through s are fixed. The only average is over the disjoint, still-fresh output layers.

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

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

24. def OAI.CubeShuffle.switchHeight line 376

    Source documentation

    Physical outward height of a switch in a butterfly.

    def switchHeight : (d : ℕ) → SwitchIndex d → ℕ
      | 0, i => nomatch i
      | d+1, Sum.inl _ => d+1
      | d+1, Sum.inr (_,i) => switchHeight d i

    Mentions: OAI.CubeShuffle.SwitchIndex

25. lemma OAI.CubeShuffle.switchHeight_le line 381
26. def OAI.CubeShuffle.AgreeThrough line 390

    Source documentation

    Equality of the already exposed outward layers.

    def AgreeThrough (d s : ℕ) (Y Y' : SwitchIndex d → Bool) : Prop :=
    …

    Mentions: OAI.CubeShuffle.SwitchIndex

27. def OAI.CubeShuffle.LayerAdapted line 394

    Source documentation

    A function of the revealed layers only.

    def LayerAdapted (d s : ℕ) {β : Type*} (f : (SwitchIndex d → Bool) → β) : Prop :=
    …

    Mentions: OAI.CubeShuffle.SwitchIndex

28. lemma OAI.CubeShuffle.agreeThrough_mono line 397
29. lemma OAI.CubeShuffle.layerAdapted_mono line 401
30. lemma OAI.CubeShuffle.layerAdapted_comp line 405
31. lemma OAI.CubeShuffle.layerAdapted_sum line 409
32. lemma OAI.CubeShuffle.assembleBits_agree line 416
33. lemma OAI.CubeShuffle.palindromeLevelCost_adapted line 429
34. lemma OAI.CubeShuffle.adapted_mul_mean_le line 463

    Source documentation

    A conditional estimate on the still-fresh layers can be multiplied by any nonnegative function of the revealed layers. This finite product-space identity is the tower argument used between non-adjacent height slabs.

    lemma adapted_mul_mean_le (r s : ℕ) (F G : (SwitchIndex (s+r) → Bool) → ℝ)
        (hF : ∀ Y, 0 ≤ F Y) (hA : LayerAdapted (s+r) s F) (B : ℝ)
        (hG : ∀ lo : Card r × SwitchIndex s → Bool,
          finiteMean (fun hi : Card s × SwitchIndex r → Bool => G (assembleBits r s lo hi)) ≤ B) :
        finiteMean (fun Y => F Y*G Y) ≤ finiteMean F * B := by
    …

    Mentions: OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.LayerAdapted, OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.assembleBits

35. theorem OAI.CubeShuffle.cycleCoefficient_decay line 486

    Source documentation

    A completely explicit FAC.5 bound. The ceiling is part of the actual finite-cycle cutoff; there is no unverified numerical certificate.

    theorem cycleCoefficient_decay (l r : ℕ) (hr : (l:ℝ)/2 ≤ r)
        (q : ℝ) (hq : 1 ≤ q) (hlog : Real.log q ≤ (l:ℝ)/250) :
        cycleCoefficient r ⌈Real.exp ((l:ℝ)/32)⌉₊ q ≤
          68 * Real.exp (-(l:ℝ)/64) := by
    …

    Mentions: OAI.CubeShuffle.cycleCoefficient

36. lemma OAI.CubeShuffle.cycleCutoff_pos line 552
37. lemma OAI.CubeShuffle.pow_sum_le_mean_powers line 561
38. def OAI.CubeShuffle.palindromeSlabCost line 574

    Source documentation

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

    noncomputable def palindromeSlabCost (l d : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (ω : BenesCoins d) : ℕ :=
    …

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

39. lemma OAI.CubeShuffle.palindromeSlabCost_adapted line 578
40. theorem OAI.CubeShuffle.palindrome_slab_partial_mgf line 587

    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 palindrome_slab_partial_mgf (r s l : ℕ) (hl : 0 < l) (hs : 2*s ≤ l)
        {ι : Type*} [Fintype ι] (e : ι ↪ Card (s+r)) (X : SwitchIndex (s+r) → Bool)
        (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^(palindromeSlabCost l (s+r) e (assembleBits r s lo hi,X))) ≤
          Real.exp (Fintype.card ι * (68*Real.exp (-(l:ℝ)/64))) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.palindromeSlabCost, OAI.CubeShuffle.assembleBits

41. lemma OAI.CubeShuffle.palindromeSlabCost_gt line 635
42. lemma OAI.CubeShuffle.palindrome_slab_adapted_mul_le line 641
43. def OAI.CubeShuffle.familyEnd line 652
44. lemma OAI.CubeShuffle.familyEnd_two line 654
45. lemma OAI.CubeShuffle.familyEnd_ge line 659
46. def OAI.CubeShuffle.palindromeFamilyCost line 667
47. lemma OAI.CubeShuffle.palindromeFamilyCost_adapted line 671
48. theorem OAI.CubeShuffle.palindrome_family_mgf line 681

    Source documentation

    Time-ordered multiplication across one family of nonadjacent slabs. The proof uses only the already proved finite conditional estimate.

    theorem palindrome_family_mgf (L n d : ℕ) (hL : 0 < L) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (X : SwitchIndex d → Bool) (q : ℝ) (hq : 1 ≤ q)
        (hlog : Real.log q ≤ 1/250) :
        finiteMean (fun Y => q^(palindromeFamilyCost L n d e (Y,X))) ≤
          Real.exp (Fintype.card ι * (68*∑ j ∈ Finset.range n,
            Real.exp (-((L*4^j:ℕ):ℝ)/64))) := by
    …

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

49. lemma OAI.CubeShuffle.pow_four_ge line 717
50. lemma OAI.CubeShuffle.sum_family_decay line 722
51. lemma OAI.CubeShuffle.palindromeLevelCost_step_add line 749
52. lemma OAI.CubeShuffle.palindromeLowCost_sum line 768

    Source documentation

    The recursive low cost is literally the sum of its physical node levels.

    lemma palindromeLowCost_sum (H d : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (ω : BenesCoins d) :
        palindromeLowCost H d e ω = ∑ i ∈ Finset.range H, palindromeLevelCost (i+1) d e ω := by
    …

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

53. lemma OAI.CubeShuffle.palindromeLowCost_slab line 781
54. lemma OAI.CubeShuffle.palindromeCost_family line 788
55. lemma OAI.CubeShuffle.finiteMean_mul_sq_le line 805
56. lemma OAI.CubeShuffle.finiteMean_mul_exp_le line 811
57. def OAI.CubeShuffle.heightDecay line 831
58. lemma OAI.CubeShuffle.heightDecay_nonneg line 834
59. lemma OAI.CubeShuffle.heightDecay_antitone line 838
60. lemma OAI.CubeShuffle.palindrome_family_mgf_decay line 849
61. theorem OAI.CubeShuffle.palindrome_high_mgf line 862

    Source documentation

    The two interlaced slab families have a uniform conditional high-level moment bound. This is FAC.6, including all dependence between families.

    theorem palindrome_high_mgf (H n d : ℕ) (hH : 0 < H) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (X : SwitchIndex d → Bool) (q : ℝ) (hq : 1 ≤ q)
        (hlog : Real.log q ≤ 1/500) :
        finiteMean (fun Y => q^(palindromeFamilyCost H n d e (Y,X)+
          palindromeFamilyCost (2*H) n d e (Y,X))) ≤ Real.exp (Fintype.card ι*heightDecay H) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.palindromeFamilyCost, OAI.CubeShuffle.heightDecay

62. lemma OAI.CubeShuffle.palindrome_high_full_mgf line 879
63. theorem OAI.CubeShuffle.palindrome_cost_mgf_cutoff line 893

    Source documentation

    Combination with the genuine sparse low-block estimate. The factor 2 in that estimate and both Cauchy steps are retained explicitly.

    theorem palindrome_cost_mgf_cutoff (r H : ℕ) (hH : 0 < H) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card (H+r)) (q : ℝ) (hq : 1 ≤ q) (hlog : Real.log q ≤ 1/1000)
        (hr : (2:ℝ)^H*((Fintype.card ι/(2:ℝ)^(H+r))*(q^2)^H) ≤ 1/2) :
        finiteMean (fun ω : BenesCoins (H+r) => q^(palindromeCost (H+r) e ω)) ≤
          Real.exp (((2:ℝ)^r*(2*((2:ℝ)^H*((Fintype.card ι/(2:ℝ)^(H+r))*(q^2)^H))^2)+
            Fintype.card ι*heightDecay H)/2) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.BenesCoins, OAI.CubeShuffle.palindromeCost, OAI.CubeShuffle.heightDecay

64. lemma OAI.CubeShuffle.cutoffMass_le line 921
65. lemma OAI.CubeShuffle.palindromeLowCost_le line 932
66. theorem OAI.CubeShuffle.palindrome_cost_mgf_coarse line 938

    Source documentation

    Dense rows are included. The cutoff-one estimate gives a uniform O(k) log moment without any small-density or dimension hypothesis.

    theorem palindrome_cost_mgf_coarse (d : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (q : ℝ) (hq : 1 ≤ q) (hlog : Real.log q ≤ 1/1000) :
        finiteMean (fun ω : BenesCoins d => q^(palindromeCost d e ω)) ≤
          Real.exp (Fintype.card ι*(1+heightDecay 1)) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.BenesCoins, OAI.CubeShuffle.palindromeCost, OAI.CubeShuffle.heightDecay

67. def OAI.CubeShuffle.momentBase line 976

    Source documentation

    The exponent remains the literal 1/1000 fixed by the manuscript.

    noncomputable def momentBase : ℝ := (2:ℝ)^(1/1000:ℝ)

68. lemma OAI.CubeShuffle.momentBase_one_le line 978
69. lemma OAI.CubeShuffle.momentBase_log line 981
70. lemma OAI.CubeShuffle.momentBase_pow line 987
71. lemma OAI.CubeShuffle.palindromeRowMoment_le_cost line 993

    Source documentation

    Remove only the source's non-increasing falling-factorial normalization; no change is made to the tuple law or the (1+a)-moment.

    lemma palindromeRowMoment_le_cost (d : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) :
        palindromeRowMoment d e (1/1000) ≤
          finiteMean (fun ω : BenesCoins d => momentBase^(palindromeCost d e ω)) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.palindromeRowMoment, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.BenesCoins, OAI.CubeShuffle.momentBase, OAI.CubeShuffle.palindromeCost

72. theorem OAI.CubeShuffle.palindrome_row_moment_coarse line 1010
73. def OAI.CubeShuffle.densityCutoff line 1018
74. lemma OAI.CubeShuffle.log_small_density line 1020
75. lemma OAI.CubeShuffle.densityCutoff_bounds line 1028
76. lemma OAI.CubeShuffle.densityCutoff_decay line 1042
77. lemma OAI.CubeShuffle.densityCutoff_power line 1054
78. lemma OAI.CubeShuffle.densityCutoff_sparse line 1075
79. lemma OAI.CubeShuffle.momentBase_log_exact line 1092
80. lemma OAI.CubeShuffle.densityCutoff_le_height line 1096
81. def OAI.CubeShuffle.densityTailConstant line 1113
82. lemma OAI.CubeShuffle.densityTailConstant_nonneg line 1116
83. lemma OAI.CubeShuffle.heightDecay_cutoff line 1120
84. lemma OAI.CubeShuffle.sparse_low_algebra line 1129
85. lemma OAI.CubeShuffle.palindrome_row_moment_small line 1138
86. def OAI.CubeShuffle.densityConstant line 1175
87. lemma OAI.CubeShuffle.densityConstant_pos line 1178
88. theorem OAI.CubeShuffle.palindrome_row_moment_bound line 1186

    Source documentation

    The absolute power improvement in the first clause of fac:density, for the actual full palindrome and all labelled distinct input tuples.

    theorem palindrome_row_moment_bound (d : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (hk : 0 < Fintype.card ι) :
        palindromeRowMoment d e (1/1000) ≤ Real.exp (densityConstant*Fintype.card ι*
            ((Fintype.card ι:ℝ)/(2:ℝ)^d)^(1/512:ℝ)) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.palindromeRowMoment, OAI.CubeShuffle.densityConstant

89. lemma OAI.CubeShuffle.palindromeRowMoment_nonneg line 1221
90. theorem OAI.CubeShuffle.palindrome_log_row_moment line 1230

    Source documentation

    Literal logarithmic row-density estimate with a=1/1000, eta=1/512, and one explicit absolute positive constant.

    theorem palindrome_log_row_moment (d : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (hk : 0 < Fintype.card ι) :
        Real.log (palindromeRowMoment d e (1/1000)) ≤ densityConstant*Fintype.card ι*
            ((Fintype.card ι:ℝ)/(2:ℝ)^d)^(1/512:ℝ) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.palindromeRowMoment, OAI.CubeShuffle.densityConstant