OAI/Probability/CubeShuffle/RecursiveDensity.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.assignmentCost line 11
2. lemma OAI.CubeShuffle.palindromeCost_eq line 19
3. lemma OAI.CubeShuffle.palindromeCost_step line 29
4. def OAI.CubeShuffle.routingMoment line 39
5. lemma OAI.CubeShuffle.routingMoment_nonneg line 45
6. lemma OAI.CubeShuffle.palindrome_matches_step line 50
7. lemma OAI.CubeShuffle.routingMoment_step line 61
8. lemma OAI.CubeShuffle.child_moment_product line 104
9. lemma OAI.CubeShuffle.palindrome_probability_step line 136
10. lemma OAI.CubeShuffle.child_power_product_bound line 151
11. lemma OAI.CubeShuffle.assignment_moment_bound line 180
12. theorem OAI.CubeShuffle.palindrome_pointwise_moment line 221

    Source documentation

    The precise recursive pointwise density estimate: the surviving power is under the actual, independent fair switch law, never an auxiliary coloring law.

    theorem palindrome_pointwise_moment (d : ℕ) {ι : Type*} [Fintype ι]
        (e f : ι ↪ Card d) (a : ℝ) (ha : 0 ≤ a) :
        (PairRouting.tupleProbability (palindromePerm d) e f)^(1+a) ≤
          (2:ℝ)^(-(d:ℝ)*Fintype.card ι*a) * routingMoment d e f a := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.PairRouting.tupleProbability, OAI.CubeShuffle.palindromePerm, OAI.CubeShuffle.routingMoment

13. lemma OAI.CubeShuffle.routingMoment_sum line 281
14. lemma OAI.CubeShuffle.finite_row_power line 303
15. def OAI.CubeShuffle.palindromeRowMoment line 312
16. lemma OAI.CubeShuffle.density_normalization line 317
17. theorem OAI.CubeShuffle.palindrome_row_density_moment line 326

    Source documentation

    Source FAC.1, for every labelled distinct tuple, with the exact falling- factorial normalization and the genuine fair-coin palindrome routing cost.

    theorem palindrome_row_density_moment (d : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card d) (a : ℝ) (ha : 0 ≤ a) :
        palindromeRowMoment d e a ≤
          (((2^d).descFactorial (Fintype.card ι):ℝ)/((2^d:ℕ):ℝ)^(Fintype.card ι))^a *
            finiteMean (fun ω : BenesCoins d => (2:ℝ)^((palindromeCost d e ω:ℝ)*a)) := by
    …

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

18. lemma OAI.CubeShuffle.subset_biUnion_indicator line 348
19. lemma OAI.CubeShuffle.cylinder_block_polynomial line 370

    Source documentation

    Positive multilinear block-polynomials are dominated by product measure whenever their supports are disjoint and all joint inclusion bounds hold.

    lemma cylinder_block_polynomial {α β Ω : Type*} [DecidableEq α] [Fintype β]
        [Fintype Ω] (τ : β → Type*) [∀ b, Fintype (τ b)]
        (F : Ω → Finset α) (p : α → ℝ)
        (hF : CylinderBound (inclusionMoment F) p)
        (T : ∀ b, τ b → Finset α) (c : ∀ b, τ b → ℝ)
        (hc : ∀ b s, 0 ≤ c b s)
        (hd : ∀ b b', b ≠ b' → ∀ s s', Disjoint (T b s) (T b' s')) :
        finiteMean (fun ω => ∏ b, ∑ s, c b s * if T b s ⊆ F ω then 1 else 0) ≤
          ∏ b, ∑ s, c b s * ∏ x ∈ T b s, p x := by
    …

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

20. def OAI.CubeShuffle.sparseCoefficient line 412
21. lemma OAI.CubeShuffle.sparseCoefficient_nonneg line 415
22. lemma OAI.CubeShuffle.sparse_block_pointwise line 420
23. lemma OAI.CubeShuffle.geometric_sum_half line 440
24. lemma OAI.CubeShuffle.sparse_binomial_bound line 449
25. lemma OAI.CubeShuffle.sparse_block_product_bound line 483
26. def OAI.CubeShuffle.sparseMass line 507
27. theorem OAI.CubeShuffle.sparse_block_mgf line 513

    Source documentation

    The sparse low-block moment bound uses only actual joint inclusion, not independence or a negative-association assumption.

    theorem sparse_block_mgf {α β Ω : Type*} [DecidableEq α] [Fintype β] [Fintype Ω]
        (D : β → Finset α) (hd : Pairwise (fun b b' => Disjoint (D b) (D b')))
        (F : Ω → Finset α) (p w : ℝ) (hp : 0 ≤ p) (hw : 0 ≤ w)
        (hF : ∀ T, inclusionMoment F T ≤ p^T.card)
        (hr : ∀ b, ((D b).card:ℝ)*(p*w) ≤ 1/2) :
        finiteMean (fun ω => w^(sparseMass D (F ω))) ≤
          Real.exp (∑ b, 2*(((D b).card:ℝ)*(p*w))^2) := by
    …

    Mentions: OAI.CubeShuffle.inclusionMoment, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.sparseMass

28. theorem OAI.CubeShuffle.inverseButterfly_sparse_mgf line 550

    Source documentation

    In particular this holds for central marks of the genuine input butterfly.

    theorem inverseButterfly_sparse_mgf (d : ℕ) {β : Type*} [Fintype β]
        (D : β → Finset (Card d)) (hd : Pairwise (fun b b' => Disjoint (D b) (D b')))
        (A : Finset (Card d)) (w : ℝ) (hw : 0 ≤ w)
        (hr : ∀ b, ((D b).card:ℝ)*((A.card/(2:ℝ)^d)*w) ≤ 1/2) :
        finiteMean (fun ω : SwitchIndex d → Bool =>
          w^(sparseMass D (inverseButterflyMarks d A ω))) ≤
          Real.exp (∑ b, 2*(((D b).card:ℝ)*((A.card/(2:ℝ)^d)*w))^2) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.SwitchIndex, OAI.CubeShuffle.sparseMass, OAI.CubeShuffle.inverseButterflyMarks

29. def OAI.CubeShuffle.crowdedMass line 565
30. lemma OAI.CubeShuffle.crowdedMass_le line 567
31. lemma OAI.CubeShuffle.crowdedMass_add line 571
32. lemma OAI.CubeShuffle.alternatingCycles_le_crowded line 575
33. lemma OAI.CubeShuffle.palindromeCost_le_crowded line 584
34. def OAI.CubeShuffle.palindromeLowCost line 609

    Source documentation

    The exact sum of FAC.1 node costs through height H.

    noncomputable def palindromeLowCost (H : ℕ) : (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

35. def OAI.CubeShuffle.cutoffMass line 623

    Source documentation

    Colliding mass in the size-2^H central blocks, read along the actual input routes.

    noncomputable def cutoffMass (H : ℕ) : (d : ℕ) → {ι : Type*} → [Fintype ι] →
        (ι ↪ Card d) → BenesCoins d → ℕ
      | 0, _, _, _, _ => 0
      | d+1, ι, _, e, ω =>
          if d+1 ≤ H then crowdedMass (Fintype.card ι) else
          let σ := benesStepEquiv d ω
    …

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

36. lemma OAI.CubeShuffle.palindromeLowCost_eq line 635
37. lemma OAI.CubeShuffle.palindromeLowCost_le_cutoff line 645
38. def OAI.CubeShuffle.centralBlock line 661
39. lemma OAI.CubeShuffle.mem_centralBlock line 664
40. lemma OAI.CubeShuffle.centralBlock_card line 676
41. lemma OAI.CubeShuffle.centralBlock_disjoint line 683
42. lemma OAI.CubeShuffle.centralBlock_zero line 692
43. lemma OAI.CubeShuffle.centralBlock_step line 698
44. lemma OAI.CubeShuffle.block_inter_step line 704
45. lemma OAI.CubeShuffle.sparseMass_central_zero line 720
46. lemma OAI.CubeShuffle.sparseMass_central_step line 726
47. lemma OAI.CubeShuffle.inverseButterfly_coordinates_step line 748
48. lemma OAI.CubeShuffle.inverseButterflyMarks_child line 759
49. lemma OAI.CubeShuffle.inverseButterflyMarks_card line 799
50. lemma OAI.CubeShuffle.benes_input_coordinates line 804
51. lemma OAI.CubeShuffle.cutoffMass_central line 810
52. theorem OAI.CubeShuffle.palindrome_low_mgf line 844

    Source documentation

    Actual low-height cycle mass of the Beneš routing, with fair input coins. There is no independence assumption on marked positions.

    theorem palindrome_low_mgf (r H : ℕ) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card (H+r)) (q : ℝ) (hq : 1 ≤ q)
        (hr : (2:ℝ)^H*((Fintype.card ι/(2:ℝ)^(H+r))*q^H) ≤ 1/2) :
        finiteMean (fun ω : BenesCoins (H+r) => q^(palindromeLowCost H (H+r) e ω)) ≤
          Real.exp ((2:ℝ)^r * (2 * ((2:ℝ)^H*((Fintype.card ι/(2:ℝ)^(H+r))*q^H))^2)) := by
    …

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