The root-declumping parent formula

Section 5.1 of the paper (source lines 2148–2229; inventory P15 and Lemma lem:root_declumping(i),(ii)). For a critical offspring law μ with μ_1 ≠ 1, a set B ⊆ ℕ and a mark G, write π = P(G(𝒯) = 1) and π̂ = P(Ghat(𝒯) = 1) for the declumped mark Ghat = declumpedMark B G (root degree in B and some marked child).

• parent_formula (eq:parent_formula): by the branching property, π̂ = E[1{D ∈ B}(1 - (1 - π)^D)] = F_B(π), F_B(p) = ∑_{j ∈ B} μ_j (1 - (1 - p)^j); more generally bienayme_real_rootDegree_mem_forall_exists computes P(k_∅ ∈ B, all children in A', some child in A) for A ⊆ A'.
• pointwise_bounds: p ≤ 1 - (1 - p)^d ≤ d p for d ≥ 1, p ∈ [0, 1]; hence bB_mul_le_declumped, declumped_le_cBReal_mul: b_B π ≤ π̂ ≤ c_B π, with b_B = P(D ∈ B, D ≥ 1) (bB_eq_prob) and c_B = ∑_{j ∈ B} j μ_j; b_B > 0 ↔ c_B > 0.
• tendsto_slopeFun, tendsto_parentFun_div, parentFun_sub_isLittleO: the derivative of F_B at zero is c_B, by dominated convergence with the summable dominating sequence j μ_j 1{j ∈ B} (finite first moment only; no second moment is assumed).
• root_declumping_bounded, root_declumping_divergent: Lemma lem:root_declumping(i),(ii) along an arbitrary filter and an arbitrary scale x → ∞.

Part (iii) of Lemma lem:root_declumping needs forest and local-limit estimates and is not proved here.

theorem PoissonDeclumping.RootDeclumping.bienayme_real_rootDegree_mem_forall (μ : PMF ℕ) (B : Set ℕ) (A : Set PlaneTree) : (PlaneTree.bienayme μ).real {T : PlaneTree | T.rootDegree ∈ B ∧ ∀ U ∈ T.children, U ∈ A} = ∑' (d : ℕ), B.indicator (fun (d : ℕ) => LeafHeight.mass μ d * (PlaneTree.bienayme μ).real A ^ d) d

P(k_∅ ∈ B, all children in A) = ∑_{d ∈ B} μ_d P(A)^d (real form).

theorem PoissonDeclumping.RootDeclumping.summable_indicator_mass_mul {μ : PMF ℕ} (B : Set ℕ) {f : ℕ → ℝ} (h0 : ∀ (d : ℕ), 0 ≤ f d) (h1 : ∀ (d : ℕ), f d ≤ 1) : Summable fun (d : ℕ) => B.indicator (fun (d : ℕ) => LeafHeight.mass μ d * f d) d

Summability of d ↦ 1_B(d) μ_d f(d) for bounded f.

theorem PoissonDeclumping.RootDeclumping.bienayme_real_rootDegree_mem_forall_exists (μ : PMF ℕ) (B : Set ℕ) {A A' : Set PlaneTree} (hAA' : A ⊆ A') : (PlaneTree.bienayme μ).real {T : PlaneTree | T.rootDegree ∈ B ∧ (∀ U ∈ T.children, U ∈ A') ∧ ∃ U ∈ T.children, U ∈ A} = ∑' (d : ℕ), B.indicator (fun (d : ℕ) => LeafHeight.mass μ d * ((PlaneTree.bienayme μ).real A' ^ d - ((PlaneTree.bienayme μ).real A' - (PlaneTree.bienayme μ).real A) ^ d)) d

General parent formula: for A ⊆ A', P(k_∅ ∈ B, all children in A', some child in A) = ∑_{d ∈ B} μ_d (P(A')^d - P(A' \ A)^d).

noncomputable def PoissonDeclumping.RootDeclumping.parentFun (μ : PMF ℕ) (B : Set ℕ) (p : ℝ) : ℝ

The function F_B(p) = ∑_{j ∈ B} μ_j (1 - (1 - p)^j) of the parent formula eq:parent_formula.

Equations

• PoissonDeclumping.RootDeclumping.parentFun μ B p = ∑' (j : ℕ), B.indicator (fun (j : ℕ) => PoissonDeclumping.LeafHeight.mass μ j * (1 - (1 - p) ^ j)) j

theorem PoissonDeclumping.RootDeclumping.parent_formula {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (B : Set ℕ) (G : PlaneTree → Prop) : (PlaneTree.bienayme μ).real {T : PlaneTree | PlaneTree.declumpedMark B G T} = parentFun μ B ((PlaneTree.bienayme μ).real {T : PlaneTree | G T})

Parent formula eq:parent_formula (source lines 2219–2224, inventory P15): for a critical μ with μ_1 ≠ 1, any B ⊆ ℕ and any mark G, with π = P(G(𝒯) = 1) and Ghat = declumpedMark B G, P(Ghat(𝒯) = 1) = E[1{D ∈ B}(1 - (1 - π)^D)] = ∑_{j ∈ B} μ_j (1-(1-π)^j).

Pointwise bounds and the constants b_B, c_B

theorem PoissonDeclumping.RootDeclumping.one_sub_one_sub_pow_nonneg {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (d : ℕ) : 0 ≤ 1 - (1 - p) ^ d

0 ≤ 1 - (1 - p)^d for p ∈ [0, 1].

theorem PoissonDeclumping.RootDeclumping.le_one_sub_one_sub_pow {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {d : ℕ} (hd : 1 ≤ d) : p ≤ 1 - (1 - p) ^ d

p ≤ 1 - (1 - p)^d for d ≥ 1 and p ∈ [0, 1] (source line 2225).

theorem PoissonDeclumping.RootDeclumping.one_sub_one_sub_pow_le {p : ℝ} (hp1 : p ≤ 1) (d : ℕ) : 1 - (1 - p) ^ d ≤ ↑d * p

1 - (1 - p)^d ≤ d p for p ≤ 1 (Bernoulli; source line 2225).

theorem PoissonDeclumping.RootDeclumping.pointwise_bounds {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {d : ℕ} (hd : 1 ≤ d) : p ≤ 1 - (1 - p) ^ d ∧ 1 - (1 - p) ^ d ≤ ↑d * p

The pointwise bounds p ≤ 1 - (1 - p)^d ≤ d p for d ≥ 1, p ∈ [0, 1].

theorem PoissonDeclumping.RootDeclumping.one_sub_one_sub_pow_eq (p : ℝ) (d : ℕ) : 1 - (1 - p) ^ d = p * ∑ i ∈ Finset.range d, (1 - p) ^ i

1 - (1 - p)^d = p ∑_{i < d} (1 - p)^i.

theorem PoissonDeclumping.RootDeclumping.geom_sum_one_sub_bounds {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (d : ℕ) : 0 ≤ ∑ i ∈ Finset.range d, (1 - p) ^ i ∧ ∑ i ∈ Finset.range d, (1 - p) ^ i ≤ ↑d

0 ≤ ∑_{i < d} (1 - p)^i ≤ d for p ∈ [0, 1].

noncomputable def PoissonDeclumping.RootDeclumping.cBReal (μ : PMF ℕ) (B : Set ℕ) : ℝ

The constant c_B = E[k_∅(𝒯) 1{k_∅(𝒯) ∈ B}] = ∑_{j ∈ B} j μ_j, in real numbers.

Equations

• PoissonDeclumping.RootDeclumping.cBReal μ B = ∑' (j : ℕ), B.indicator (fun (j : ℕ) => ↑j * PoissonDeclumping.LeafHeight.mass μ j) j

noncomputable def PoissonDeclumping.RootDeclumping.bB (μ : PMF ℕ) (B : Set ℕ) : ℝ

The constant b_B = P(k_∅(𝒯) ∈ B, k_∅(𝒯) ≥ 1) = ∑_{j ∈ B, j ≥ 1} μ_j.

Equations

• PoissonDeclumping.RootDeclumping.bB μ B = ∑' (j : ℕ), {j : ℕ | j ∈ B ∧ 1 ≤ j}.indicator (PoissonDeclumping.LeafHeight.mass μ) j

theorem PoissonDeclumping.RootDeclumping.summable_cB {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : Summable fun (j : ℕ) => B.indicator (fun (j : ℕ) => ↑j * LeafHeight.mass μ j) j

theorem PoissonDeclumping.RootDeclumping.summable_bB {μ : PMF ℕ} (B : Set ℕ) : Summable fun (j : ℕ) => {j : ℕ | j ∈ B ∧ 1 ≤ j}.indicator (LeafHeight.mass μ) j

theorem PoissonDeclumping.RootDeclumping.cBReal_nonneg {μ : PMF ℕ} (B : Set ℕ) : 0 ≤ cBReal μ B

theorem PoissonDeclumping.RootDeclumping.bB_nonneg {μ : PMF ℕ} (B : Set ℕ) : 0 ≤ bB μ B

theorem PoissonDeclumping.RootDeclumping.bB_le_cBReal {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : bB μ B ≤ cBReal μ B

b_B ≤ c_B (critical μ).

theorem PoissonDeclumping.RootDeclumping.cBReal_le_one {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : cBReal μ B ≤ 1

c_B ≤ 1 (critical μ).

theorem PoissonDeclumping.RootDeclumping.bB_pos_iff_cBReal_pos {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : 0 < bB μ B ↔ 0 < cBReal μ B

b_B > 0 if and only if c_B > 0: both say that μ charges some j ∈ B with j ≥ 1.

@[simp]

theorem PoissonDeclumping.RootDeclumping.parentFun_zero {μ : PMF ℕ} (B : Set ℕ) : parentFun μ B 0 = 0

π ↦ F_B(π) vanishes at zero.

theorem PoissonDeclumping.RootDeclumping.parentFun_nonneg {μ : PMF ℕ} (B : Set ℕ) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : 0 ≤ parentFun μ B p

theorem PoissonDeclumping.RootDeclumping.bB_mul_le_parentFun {μ : PMF ℕ} (B : Set ℕ) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : bB μ B * p ≤ parentFun μ B p

Lower bound b_B π ≤ F_B(π) (source line 2226).

theorem PoissonDeclumping.RootDeclumping.parentFun_le_cBReal_mul {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : parentFun μ B p ≤ cBReal μ B * p

Upper bound F_B(π) ≤ c_B π (source line 2226).

Derivative at zero, by dominated convergence (finite first moment only)

noncomputable def PoissonDeclumping.RootDeclumping.slopeFun (μ : PMF ℕ) (B : Set ℕ) (p : ℝ) : ℝ

ψ_B(p) = ∑_{j ∈ B} μ_j ∑_{i < j} (1 - p)^i, so that F_B(p) = p ψ_B(p) and ψ_B(0) = c_B.

Equations

• PoissonDeclumping.RootDeclumping.slopeFun μ B p = ∑' (j : ℕ), B.indicator (fun (j : ℕ) => PoissonDeclumping.LeafHeight.mass μ j * ∑ i ∈ Finset.range j, (1 - p) ^ i) j

theorem PoissonDeclumping.RootDeclumping.parentFun_eq_mul_slopeFun {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : parentFun μ B p = p * slopeFun μ B p

theorem PoissonDeclumping.RootDeclumping.slopeFun_zero {μ : PMF ℕ} (B : Set ℕ) : slopeFun μ B 0 = cBReal μ B

theorem PoissonDeclumping.RootDeclumping.tendsto_slopeFun {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : Filter.Tendsto (slopeFun μ B) (nhdsWithin 0 (Set.Ici 0)) (nhds (cBReal μ B))

Dominated convergence (source lines 2226–2228), with the dominating sequence j μ_j 1{j ∈ B}, which is summable by criticality (finite first moment); no second moment is used: ψ_B(p) → c_B as p ↓ 0.

theorem PoissonDeclumping.RootDeclumping.tendsto_parentFun_div {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : Filter.Tendsto (fun (p : ℝ) => parentFun μ B p / p) (nhdsWithin 0 (Set.Ioi 0)) (nhds (cBReal μ B))

F_B(π) / π → c_B as π ↓ 0 (source lines 2226–2228).

theorem PoissonDeclumping.RootDeclumping.parentFun_sub_isLittleO {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) : (fun (p : ℝ) => parentFun μ B p - cBReal μ B * p) =o[nhdsWithin 0 (Set.Ici 0)] fun (p : ℝ) => p

F_B(π) - c_B π = o(π) as π ↓ 0, including π = 0.

Probabilistic form: b_B π ≤ π̂ ≤ c_B π and Lemma lem:root_declumping(i),(ii)

theorem PoissonDeclumping.RootDeclumping.bB_eq_prob {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (B : Set ℕ) : bB μ B = (PlaneTree.bienayme μ).real {T : PlaneTree | T.rootDegree ∈ B ∧ 1 ≤ T.rootDegree}

b_B = P(k_∅(𝒯) ∈ B, k_∅(𝒯) ≥ 1).

theorem PoissonDeclumping.RootDeclumping.bB_mul_le_declumped {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (B : Set ℕ) (G : PlaneTree → Prop) : bB μ B * (PlaneTree.bienayme μ).real {T : PlaneTree | G T} ≤ (PlaneTree.bienayme μ).real {T : PlaneTree | PlaneTree.declumpedMark B G T}

π̂ ≥ b_B π (source line 2210): P(Ghat(𝒯) = 1) ≥ b_B P(G(𝒯) = 1).

theorem PoissonDeclumping.RootDeclumping.declumped_le_cBReal_mul {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (B : Set ℕ) (G : PlaneTree → Prop) : (PlaneTree.bienayme μ).real {T : PlaneTree | PlaneTree.declumpedMark B G T} ≤ cBReal μ B * (PlaneTree.bienayme μ).real {T : PlaneTree | G T}

π̂ ≤ c_B π (source line 2226).

theorem PoissonDeclumping.RootDeclumping.root_declumping_bounded {μ : PMF ℕ} {ι : Type u_1} {l : Filter ι} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (B : Set ℕ) (G : ι → PlaneTree → Prop) (x : ι → ℝ) (hx : Filter.Tendsto x l Filter.atTop) (hbdd : ∃ (C : ℝ), ∀ᶠ (i : ι) in l, x i * (PlaneTree.bienayme μ).real {T : PlaneTree | G i T} ≤ C) : Filter.Tendsto (fun (i : ι) => x i * (PlaneTree.bienayme μ).real {T : PlaneTree | PlaneTree.declumpedMark B (G i) T} - cBReal μ B * (x i * (PlaneTree.bienayme μ).real {T : PlaneTree | G i T})) l (nhds 0)

Lemma lem:root_declumping(i) (source lines 2206–2207, 2226–2229), for an arbitrary filter l and scale x → ∞ (the paper: x = n → ∞ along admissible sizes): if the raw mean x π is eventually bounded, then x π̂ - c_B x π → 0. Only criticality (finite first moment) is used; no second moment.

theorem PoissonDeclumping.RootDeclumping.root_declumping_divergent {μ : PMF ℕ} {ι : Type u_1} {l : Filter ι} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (B : Set ℕ) (hb : 0 < bB μ B) (G : ι → PlaneTree → Prop) (x : ι → ℝ) (hdiv : Filter.Tendsto (fun (i : ι) => x i * (PlaneTree.bienayme μ).real {T : PlaneTree | G i T}) l Filter.atTop) : Filter.Tendsto (fun (i : ι) => x i * (PlaneTree.bienayme μ).real {T : PlaneTree | PlaneTree.declumpedMark B (G i) T}) l Filter.atTop

Lemma lem:root_declumping(ii) (source line 2208), for an arbitrary filter: if b_B > 0 and the raw mean x π diverges, then the declumped mean x π̂ diverges.