Documentation

LeanPool.RareSubtreePatterns.Bridge.ForestEstimates

Forest estimates: Lemma lem:forest_estimates #

Work package WP2b of the bridge plan. Source lines 1119–1180 (Lemma 3.5 and its proof, inventory L3.5, proof step P03), 1328–1342 (P(|𝒯| = n) ≍ 1 / (n a_n), B11).

Notation: 𝒒_β„“ is a forest of β„“ independent ΞΌ-BienaymΓ© trees, P(|𝒒_β„“| = q) is (forestSizeWeight ΞΌ β„“ q).toReal, Ξ¨_m(x) = walkProb ΞΌ m x (zero for negative time) and supWalk ΞΌ m = sup_x Ξ¨_m(x).

Main statements #

The paper states the estimates for β„“ β‰₯ 1; the empty forest β„“ = 0 (|𝒒_0| = 0) is handled separately here (forestSizeWeight_zero_left) and all bounds hold for every β„“. In the periodic case the paper's second estimate divides by Ξ¨_n(-1) and is later applied at times n - c where Ξ¨_{n-c}(-1) may vanish; the numerator form avoids this (correction F3).

sup_x Ξ¨_m(x) #

source
noncomputable def PoissonDeclumping.Bridge.supWalk (ΞΌ : PMF β„•) (m : β„€) :
ℝ

supWalk ΞΌ m = sup_x Ξ¨_m(x) (zero for negative m).

Equations
Instances For
    source
    theorem PoissonDeclumping.Bridge.bddAbove_range_walkProb (ΞΌ : PMF β„•) (m : β„€) :
    BddAbove (Set.range (walkProb ΞΌ m))
    source
    theorem PoissonDeclumping.Bridge.walkProb_le_supWalk (ΞΌ : PMF β„•) (m x : β„€) :
    walkProb ΞΌ m x ≀ supWalk ΞΌ m
    source
    theorem PoissonDeclumping.Bridge.supWalk_nonneg (ΞΌ : PMF β„•) (m : β„€) :
    0 ≀ supWalk ΞΌ m
    source
    theorem PoissonDeclumping.Bridge.supWalk_le_one (ΞΌ : PMF β„•) (m : β„€) :
    supWalk ΞΌ m ≀ 1
    source
    theorem PoissonDeclumping.Bridge.supWalk_of_neg (ΞΌ : PMF β„•) {m : β„€} (hm : m < 0) :
    supWalk ΞΌ m = 0
    source
    theorem PoissonDeclumping.Bridge.exists_supWalk_le {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), 0 ≀ C ∧ βˆ€ (m : β„•), 1 ≀ m β†’ supWalk ΞΌ ↑m ≀ C / a m

    sup_x Ξ¨_m(x) ≀ C / a_m for every m β‰₯ 1 (field sup_le).

    source
    theorem PoissonDeclumping.Bridge.exists_supWalk_le_of_le_two_mul {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), 0 ≀ C ∧ βˆ€ (n m : β„•), 1 ≀ n β†’ 1 ≀ m β†’ n ≀ 2 * m β†’ supWalk ΞΌ ↑m ≀ C / a n

    sup_x Ξ¨_m(x) ≀ C / a_n whenever n ≀ 2m (exists_le_div_of_le_two_mul).

    The empty forest and total masses #

    source
    theorem PoissonDeclumping.Bridge.forestSizeWeight_zero_left (ΞΌ : PMF β„•) (q : β„•) :
    PlaneTree.forestSizeWeight ΞΌ 0 q = if q = 0 then 1 else 0

    The empty forest has 0 vertices: P(|𝒒_0| = q) = 1{q = 0}.

    source
    theorem PoissonDeclumping.Bridge.tsum_forestSizeWeight_le_one (ΞΌ : PMF β„•) (β„“ : β„•) :
    βˆ‘' (q : β„•), PlaneTree.forestSizeWeight ΞΌ β„“ q ≀ 1
    source
    theorem PoissonDeclumping.Bridge.summable_forestSizeWeight_toReal (ΞΌ : PMF β„•) (β„“ : β„•) :
    Summable fun (q : β„•) => (PlaneTree.forestSizeWeight ΞΌ β„“ q).toReal

    Local bounds #

    source
    theorem PoissonDeclumping.Bridge.forestSizeWeight_toReal_le {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), 0 ≀ C ∧ βˆ€ (β„“ q : β„•), 1 ≀ q β†’ (PlaneTree.forestSizeWeight ΞΌ β„“ q).toReal ≀ C * ↑ℓ / (↑q * a q)

    Local forest bound (source lines 1137–1141): there is C β‰₯ 0 with P(|𝒒_β„“| = q) ≀ C β„“ / (q a_q) for all β„“ and all q β‰₯ 1.

    source
    theorem PoissonDeclumping.Bridge.forest_local_le {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), βˆ€ (β„“ N : β„•), 1 ≀ β„“ β†’ 1 ≀ N β†’ (PlaneTree.forestSizeWeight ΞΌ β„“ N).toReal ≀ C * ↑ℓ / (↑N * a N)

    Lemma lem:forest_estimates, local form (plan WP2b.4): one C with P(|𝒒_β„“| = N) ≀ C β„“ / (N a_N) for β„“, N β‰₯ 1.

    source
    theorem PoissonDeclumping.Bridge.tree_size_asymp {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (c : ℝ) (C : ℝ), 0 < c ∧ βˆ€ (n : β„•), 1 ≀ n β†’ PlaneTree.Admissible ΞΌ n β†’ c / (↑n * a n) ≀ (PlaneTree.bienayme ΞΌ).real {T : PlaneTree | T.vertexCount = n} ∧ (PlaneTree.bienayme ΞΌ).real {T : PlaneTree | T.vertexCount = n} ≀ C / (↑n * a n)

    P(|𝒯| = n) ≍ 1 / (n a_n) along admissible sizes (source line 1329, B11): one pair c > 0, C with c / (n a_n) ≀ P(|𝒯| = n) ≀ C / (n a_n) at every admissible n β‰₯ 1.

    The forest-size tail (first estimate of Lemma 3.5) #

    source
    theorem PoissonDeclumping.Bridge.forest_tail_le {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), 0 ≀ C ∧ βˆ€ (β„“ m : β„•), 1 ≀ m β†’ βˆ‘' (q : β„•), (Set.Ioi m).indicator (fun (q : β„•) => (PlaneTree.forestSizeWeight ΞΌ β„“ q).toReal) q ≀ C * ↑ℓ / a m

    Lemma lem:forest_estimates, first estimate (source lines 1124–1148): one C with P(|𝒒_β„“| > m) ≀ C β„“ / a_m for every β„“ and every m β‰₯ 1.

    The bridge-weighted tail (second estimate of Lemma 3.5, numerator form) #

    source
    theorem PoissonDeclumping.Bridge.forest_weighted_tail_sup_le {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), 0 ≀ C ∧ βˆ€ (β„“ m N : β„•), 1 ≀ m β†’ 2 * m ≀ N β†’ βˆ‘' (q : β„•), (Set.Ioi m).indicator (fun (q : β„•) => (PlaneTree.forestSizeWeight ΞΌ β„“ q).toReal * supWalk ΞΌ (↑N - ↑q)) q ≀ C * ↑ℓ / (a m * a N)

    Lemma lem:forest_estimates, second estimate, numerator form (source lines 1149–1179, corrections F3/F12): one C such that for all β„“, all m β‰₯ 1 and all N β‰₯ 2m, E[sup_x Ξ¨_{N-|𝒒_β„“|}(x) 1{|𝒒_β„“| > m}] ≀ C β„“ / (a_m a_N). The sum is split at q = N/2: for q ≀ N/2, sup_x Ξ¨_{N-q} ≀ C / a_N; for N/2 < q ≀ N, P(|𝒒_β„“| = q) ≀ C β„“ / (N a_N) and βˆ‘_{h ≀ N} sup_x Ξ¨_h ≀ 1 + C N / a_N (Karamata; the term h = 0 is Ξ¨_0(0) = 1); q > N contributes nothing.

    source
    theorem PoissonDeclumping.Bridge.forest_weighted_tail_le {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), βˆ€ (β„“ m N : β„•), 1 ≀ m β†’ 2 * m ≀ N β†’ βˆ€ (e : β„• β†’ β„€), βˆ‘' (q : β„•), (Set.Ioi m).indicator (fun (q : β„•) => (PlaneTree.forestSizeWeight ΞΌ β„“ q).toReal * walkProb ΞΌ (↑N - ↑q) (e q)) q ≀ C * ↑ℓ / (a m * a N)

    Lemma lem:forest_estimates, second estimate, numerator form with an endpoint selector (plan WP2b.2): one C such that for all β„“, m β‰₯ 1, N β‰₯ 2m and every e : β„• β†’ β„€, βˆ‘_{q > m} P(|𝒒_β„“| = q) Ξ¨_{N-q}(e q) ≀ C β„“ / (a_m a_N) (the selector e encodes sup_x).

    source
    theorem PoissonDeclumping.Bridge.forest_weighted_tail_div_le {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), βˆ€ (β„“ m n : β„•), 1 ≀ m β†’ 2 * m ≀ n β†’ PlaneTree.Admissible ΞΌ n β†’ βˆ€ (e : β„• β†’ β„€), (walkProb ΞΌ (↑n) (-1))⁻¹ * βˆ‘' (q : β„•), (Set.Ioi m).indicator (fun (q : β„•) => (PlaneTree.forestSizeWeight ΞΌ β„“ q).toReal * walkProb ΞΌ (↑n - ↑q) (e q)) q ≀ C * ↑ℓ / a m

    Lemma lem:forest_estimates, second estimate, the paper's form (source lines 1127–1132): one C such that for all β„“, m β‰₯ 1, admissible n β‰₯ 2m and every e : β„• β†’ β„€, Ξ¨_n(-1)⁻¹ E[Ξ¨_{n-|𝒒_β„“|}(e |𝒒_β„“|) 1{|𝒒_β„“| > m}] ≀ C β„“ / a_m (Ξ¨_n(-1) β‰₯ c / a_n).

    ENNReal forms (for lintegral computations) #

    source
    theorem PoissonDeclumping.Bridge.ofReal_indicator_toReal {s : Set β„•} {f : β„• β†’ ENNReal} (hf : βˆ€ (q : β„•), f q β‰  ⊀) (q : β„•) :
    ENNReal.ofReal (s.indicator (fun (q : β„•) => (f q).toReal) q) = s.indicator f q
    source
    theorem PoissonDeclumping.Bridge.forestSizeWeight_tail_le_ofReal {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), 0 ≀ C ∧ βˆ€ (β„“ m : β„•), 1 ≀ m β†’ βˆ‘' (q : β„•), (Set.Ioi m).indicator (PlaneTree.forestSizeWeight ΞΌ β„“) q ≀ ENNReal.ofReal (C * ↑ℓ / a m)

    ENNReal form of forest_tail_le.

    source
    theorem PoissonDeclumping.Bridge.forestSizeWeight_weighted_tail_le_ofReal {ΞΌ : PMF β„•} {Ξ± : ℝ} {a : β„• β†’ ℝ} (hT : StableToolkit ΞΌ Ξ± a) :
    βˆƒ (C : ℝ), 0 ≀ C ∧ βˆ€ (β„“ m N : β„•), 1 ≀ m β†’ 2 * m ≀ N β†’ βˆ‘' (q : β„•), (Set.Ioi m).indicator (fun (q : β„•) => PlaneTree.forestSizeWeight ΞΌ β„“ q * ENNReal.ofReal (supWalk ΞΌ (↑N - ↑q))) q ≀ ENNReal.ofReal (C * ↑ℓ / (a m * a N))

    ENNReal form of forest_weighted_tail_sup_le.