OAI/Probability/CubeShuffle/ModifiedDensity.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubeShuffle.exceptionChild line 7
2. lemma OAI.CubeShuffle.mem_exceptionChild line 10
3. lemma OAI.CubeShuffle.exceptionChild_card_add line 15
4. def OAI.CubeShuffle.seedSplitEquiv line 25
5. def OAI.CubeShuffle.seedSandwichShuffle line 37
6. abbrev OAI.CubeShuffle.ModifiedCoins line 44
7. def OAI.CubeShuffle.modifiedStepEquiv line 46
8. def OAI.CubeShuffle.modifiedPerm line 51
9. def OAI.CubeShuffle.modifiedCost line 56
10. lemma OAI.CubeShuffle.modifiedBoundary_cons line 60
11. lemma OAI.CubeShuffle.modifiedInputTree_node line 68
12. lemma OAI.CubeShuffle.modifiedPerm_step line 84
13. lemma OAI.CubeShuffle.modifiedPerm_coordinates line 98
14. lemma OAI.CubeShuffle.InputTree.lowCost_node line 108
15. def OAI.CubeShuffle.modifiedAssignmentCost line 137
16. lemma OAI.CubeShuffle.modifiedCost_step line 145
17. lemma OAI.CubeShuffle.PairRouting.childEmbedding_surjective line 169
18. lemma OAI.CubeShuffle.PairRouting.uniformPerm_tuple_upper line 180
19. def OAI.CubeShuffle.centralFactor line 206
20. lemma OAI.CubeShuffle.centralFactor_nonneg line 209
21. lemma OAI.CubeShuffle.centralFactor_step line 212
22. lemma OAI.CubeShuffle.modifiedPerm_zero line 223
23. lemma OAI.CubeShuffle.modifiedCost_zero line 232
24. lemma OAI.CubeShuffle.centralFactor_zero line 237
25. lemma OAI.CubeShuffle.modified_probability_zero_le line 255
26. def OAI.CubeShuffle.modifiedRoutingMoment line 278
27. lemma OAI.CubeShuffle.modifiedRoutingMoment_nonneg line 284
28. lemma OAI.CubeShuffle.modifiedRoutingMoment_zero line 290
29. lemma OAI.CubeShuffle.modified_pointwise_zero line 296
30. lemma OAI.CubeShuffle.modified_matches_step line 319
31. lemma OAI.CubeShuffle.modifiedRoutingMoment_step line 330
32. lemma OAI.CubeShuffle.modified_child_moment_product line 374
33. lemma OAI.CubeShuffle.modified_probability_step line 406
34. lemma OAI.CubeShuffle.modified_assignment_moment_bound line 428
35. lemma OAI.CubeShuffle.modified_child_power_product_bound line 472
36. theorem OAI.CubeShuffle.modified_pointwise_moment line 518

    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 modified_pointwise_moment (L r : ℕ) (E : Finset (Card r)) {ι : Type*} [Fintype ι]
        (e f : ι ↪ Card (L+r)) (he : Function.Surjective e) (a : ℝ) (ha : 0 ≤ a) :
        (PairRouting.tupleProbability (modifiedPerm L r E) e f)^(1+a) ≤
          ((2:ℝ)^(-(r:ℝ)*Fintype.card ι*a)*centralFactor L r E a) * modifiedRoutingMoment L r E e f a := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.PairRouting.tupleProbability, OAI.CubeShuffle.modifiedPerm, OAI.CubeShuffle.centralFactor, OAI.CubeShuffle.modifiedRoutingMoment

37. lemma OAI.CubeShuffle.modifiedRoutingMoment_sum line 586
38. def OAI.CubeShuffle.modifiedRowMoment line 608
39. lemma OAI.CubeShuffle.full_tuple_card line 613
40. lemma OAI.CubeShuffle.exception_card_le line 618
41. def OAI.CubeShuffle.modifiedNormalization line 621
42. lemma OAI.CubeShuffle.modifiedNormalization_pos line 625
43. lemma OAI.CubeShuffle.modified_normalization_identity line 628
44. theorem OAI.CubeShuffle.modified_row_density_moment line 643

    Source documentation

    FAC.2 with the exact finite factorial normalization and actual modified law.

    theorem modified_row_density_moment (L r : ℕ) (E : Finset (Card r)) {ι : Type*} [Fintype ι]
        (e : ι ↪ Card (L+r)) (he : Function.Surjective e) (a : ℝ) (ha : 0 ≤ a) :
        modifiedRowMoment L r E e a ≤ modifiedNormalization L r E ^ a *
          finiteMean (fun ω : ModifiedCoins L r => (2:ℝ)^((modifiedCost L r E e ω:ℝ)*a)) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.modifiedRowMoment, OAI.CubeShuffle.modifiedNormalization, OAI.CubeShuffle.finiteMean, OAI.CubeShuffle.ModifiedCoins, OAI.CubeShuffle.modifiedCost

45. lemma OAI.CubeShuffle.modified_total_cost_mgf line 660
46. lemma OAI.CubeShuffle.modifiedRowMoment_bound line 673
47. lemma OAI.CubeShuffle.log_factorial_upper line 689
48. lemma OAI.CubeShuffle.log_modifiedNormalization line 707
49. lemma OAI.CubeShuffle.log_modifiedNormalization_le line 717
50. lemma OAI.CubeShuffle.modified_moment_exponential line 729
51. lemma OAI.CubeShuffle.log_power_factorial_le line 740
52. lemma OAI.CubeShuffle.modified_moment_exception_bound line 751
53. lemma OAI.CubeShuffle.heightDecay_tendsto line 770
54. def OAI.CubeShuffle.modifiedOverhead line 782
55. lemma OAI.CubeShuffle.modifiedOverhead_tendsto line 785
56. theorem OAI.CubeShuffle.modified_arbitrarily_small_rate line 803

    Source documentation

    The second quantitative row-density assertion: after fixing the absolute block size and then the exceptional fraction, every sufficiently large full permutation row has logarithmic moment rate as small as prescribed.

    theorem modified_arbitrarily_small_rate (η : ℝ) (hη : 0 < η) :
        ∃ L : ℕ, 0 < L ∧ ∃ ε : ℝ, 0 < ε ∧ ε < 1/2 ∧
          ∀ᶠ r : ℕ in Filter.atTop, ∀ (E : Finset (Card r)), (E.card:ℝ) ≤ ε*(2:ℝ)^r →
            ∀ (e : Card (L+r) ↪ Card (L+r)),
              modifiedRowMoment L r E e (1/1000) ≤ Real.exp (η*(2:ℝ)^(L+r)) := by
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.modifiedRowMoment