Local and bridge-weighted tail bounds for finite forest sizes

The total forest weight is proved from the existing finite-tree weights and the Bienaymé law. For every offspring PMF it is at most one. The local and tail bounds then follow from StableDomain, the scalar local limit theorem, Kemperman's identity, and regular variation. No extra estimate package is assumed, and positivity of the normalizer is used only at positive times. The lower size bound and the normalized bridge bound retain explicit admissibility; periodic offspring laws are allowed.

Adapted from PoissonDeclumping/Bienayme/Basic.lean and PoissonDeclumping/Bridge/ForestEstimates.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0). The source uses tuples of its own finite trees; here all sums use the existing BGW.forestWeight on lists of BGW.PlaneTree. The lower endpoint bound adapts the finite-minimum argument of PoissonDeclumping/Setup/Toolkit.lean directly to the proved lattice local limit theorem, without a toolkit hypothesis.

theorem BGW.StableTrees.Scalar.tsum_forestWeight (p : ℕ → ENNReal) (ℓ : ℕ) : ∑' (n : ℕ), forestWeight p ℓ n = (∑' (t : PlaneTree), PlaneTree.weight p t) ^ ℓ

Summing over sizes gives the product of the total weights of the component trees.

theorem BGW.StableTrees.Scalar.forestWeight_zero_left (p : ℕ → ENNReal) (n : ℕ) : forestWeight p 0 n = if n = 0 then 1 else 0

The empty forest has zero vertices and weight one.

theorem BGW.StableTrees.Scalar.tsum_forestWeight_le_one (μ : PMF ℕ) (ℓ : ℕ) : ∑' (n : ℕ), forestWeight (⇑μ) ℓ n ≤ 1

For every offspring law, the finite forests have total weight at most one.

theorem BGW.StableTrees.Scalar.tsum_forestWeight_eq_one {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (ℓ : ℕ) : ∑' (n : ℕ), forestWeight (⇑μ) ℓ n = 1

For a critical law other than the point mass at one, finite forests have total mass one.

theorem BGW.StableTrees.Scalar.forestWeight_le_one (μ : PMF ℕ) (ℓ n : ℕ) : forestWeight (⇑μ) ℓ n ≤ 1

theorem BGW.StableTrees.Scalar.forestWeight_ne_top (μ : PMF ℕ) (ℓ n : ℕ) : forestWeight (⇑μ) ℓ n ≠ ⊤

theorem BGW.StableTrees.Scalar.summable_forestWeight_toReal (μ : PMF ℕ) (ℓ : ℕ) : Summable fun (n : ℕ) => (forestWeight (⇑μ) ℓ n).toReal

theorem BGW.StableTrees.Scalar.forestWeight_toReal_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ℓ q : ℕ), 1 ≤ q → (forestWeight (⇑μ) ℓ q).toReal ≤ C * ↑ℓ / (↑q * a q)

The local forest-size bound, uniform in the number of components and positive size.

theorem BGW.StableTrees.Scalar.forest_tail_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ℓ m : ℕ), 1 ≤ m → ∑' (q : ℕ), (Set.Ioi m).indicator (fun (q : ℕ) => (forestWeight (⇑μ) ℓ q).toReal) q ≤ C * ↑ℓ / a m

The forest-size tail bound, with no restriction on the number of components.

theorem BGW.StableTrees.Scalar.walkProb_of_neg (μ : PMF ℕ) {m : ℤ} (hm : m < 0) (i : ℤ) : walkProb μ m i = 0

Negative times have zero walk mass.

theorem BGW.StableTrees.Scalar.walkProb_nonneg (μ : PMF ℕ) (m i : ℤ) : 0 ≤ walkProb μ m i

theorem BGW.StableTrees.Scalar.walkProb_le_one (μ : PMF ℕ) (m i : ℤ) : walkProb μ m i ≤ 1

noncomputable def BGW.StableTrees.Scalar.supWalk (μ : PMF ℕ) (m : ℤ) : ℝ

The supremum of the walk's point masses, also defined at negative times.

Equations

• BGW.StableTrees.Scalar.supWalk μ m = ⨆ (x : ℤ), BGW.StableTrees.walkProb μ m x

theorem BGW.StableTrees.Scalar.bddAbove_range_walkProb (μ : PMF ℕ) (m : ℤ) : BddAbove (Set.range (walkProb μ m))

theorem BGW.StableTrees.Scalar.walkProb_le_supWalk (μ : PMF ℕ) (m x : ℤ) : walkProb μ m x ≤ supWalk μ m

theorem BGW.StableTrees.Scalar.supWalk_nonneg (μ : PMF ℕ) (m : ℤ) : 0 ≤ supWalk μ m

theorem BGW.StableTrees.Scalar.supWalk_le_one (μ : PMF ℕ) (m : ℤ) : supWalk μ m ≤ 1

theorem BGW.StableTrees.Scalar.supWalk_of_neg (μ : PMF ℕ) {m : ℤ} (hm : m < 0) : supWalk μ m = 0

theorem BGW.StableTrees.Scalar.exists_supWalk_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m : ℕ), 1 ≤ m → supWalk μ ↑m ≤ C / a m

The local bound for the supremum of the point masses.

theorem BGW.StableTrees.Scalar.exists_supWalk_le_of_le_two_mul {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n m : ℕ), 1 ≤ n → 1 ≤ m → n ≤ 2 * m → supWalk μ ↑m ≤ C / a n

The local bound at comparable positive times.

theorem BGW.StableTrees.Scalar.forest_weighted_tail_sup_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableDomain μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ℓ m N : ℕ), 1 ≤ m → 2 * m ≤ N → ∑' (q : ℕ), (Set.Ioi m).indicator (fun (q : ℕ) => (forestWeight (⇑μ) ℓ q).toReal * supWalk μ (↑N - ↑q)) q ≤ C * ↑ℓ / (a m * a N)

The bridge-weighted forest tail in numerator form. Negative remaining times contribute zero, and the zero-time term is handled without using a 0.

theorem BGW.StableTrees.Scalar.exists_lower_bound_neg_one {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → 0 < walkProb μ (↑n) (-1) → c / a n ≤ walkProb μ (↑n) (-1)

A lower bound at every positive time where the endpoint -1 has positive mass. The lattice local limit theorem handles large times; a finite minimum handles the rest.

theorem BGW.StableTrees.Scalar.tree_size_asymp {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 ≤ C ∧ ∀ (n : ℕ), 1 ≤ n → (LocallyFinite.bienaymeLaw μ.toMeasure) (LocallyFinite.sizeEvent n) ≠ 0 → c / (↑n * a n) ≤ (LocallyFinite.bienaymeLaw μ.toMeasure).real (LocallyFinite.sizeEvent n) ∧ (LocallyFinite.bienaymeLaw μ.toMeasure).real (LocallyFinite.sizeEvent n) ≤ C / (↑n * a n)

The size law is bounded above and below by 1 / (n * a n) at its admissible sizes.

theorem BGW.StableTrees.Scalar.forest_weighted_tail_sup_div_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ℓ m N : ℕ), 1 ≤ m → 2 * m ≤ N → 0 < walkProb μ (↑N) (-1) → (∑' (q : ℕ), (Set.Ioi m).indicator (fun (q : ℕ) => (forestWeight (⇑μ) ℓ q).toReal * supWalk μ (↑N - ↑q)) q) / walkProb μ (↑N) (-1) ≤ C * ↑ℓ / a m

The normalized bridge-weighted tail at admissible endpoint times. The explicit positivity premise retains the lattice restriction.