Inherited microscopicity for declumped marks: Lemma lem:root_declumping(iii)

Work package WP3.5 of the bridge plan. Source lines 2197–2299 (Lemma 5.1, proof step P16). Parts (i), (ii) and the parent formula are in RootDeclumping/ParentFormula.lean and RootDeclumping/Lemma51.lean; this file proves part (iii).

Notation: Ghat = declumpedMark B G (root degree in B and some marked child), D the root degree, 𝒢_ℓ a forest of ℓ independent Bienaymé trees, c_B = cB μ B.

Main statements

• lintegral_declumped_le (branching property and union bound over the marked child): E[1{Ghat(𝒯)} Φ(|𝒯|)] ≤ ∑_{d ∈ B} d μ_d E[1{G(𝒯)} ∑_q P(|𝒢_{d-1}| = q) Φ(1 + |𝒯| + q)], and lintegral_declumped_le_of_bound, its form under a pointwise bound A(t) + κ(d).
• tsum_forestSizeWeight_mul_walkProb (eq:parent_convolution): ∑_q P(|𝒢_ℓ| = q) Ψ_{N-q}(0) = Ψ_N(-ℓ) ≤ sup_x Ψ_N(x).
• forest_bound_unweighted, forest_bound_weighted (eq:parent_forest with the truncation by 1): for a marked child t and d ≥ 1, the other d - 1 children contribute at most 1{|t| > M/4} (sup_x Ψ_{n-1-|t|}(x)) + (K / a_n) min(1, d / a_{⌊M/2⌋}).
• tendsto_tsum_min_div: ∑_{d ∈ B} d μ_d min(1, d / a_{m_n}) → 0 (dominated convergence).
• microscopic_declumped (Lemma lem:root_declumping(iii)): (S) for (G_k) and c_B ∈ (0, ∞) imply (M) for (Ghat_k) with the same cutoff.

Departure from the paper (periodic case, correction F3): the bridge-weighted estimate is used in numerator form with the time shift j = 1 of consequenceM_weighted_sup, instead of "replacing n by n - 1" in a ratio with Ψ_{n-1}(-1) (which vanishes for d ≥ 2 at admissible n); the denominator Ψ_n(-1) ≥ c / a_n enters only in microscopic_of_large.

The branching decomposition at a marked child

theorem PoissonDeclumping.Bridge.lintegral_bienayme_eq_tsum (μ : PMF ℕ) (f : PlaneTree → ENNReal) : ∫⁻ (T : PlaneTree), f T ∂PlaneTree.bienayme μ = ∑' (T : PlaneTree), PlaneTree.weight μ T * f T

E[f(𝒯)] = ∑_T w(T) f(T).

theorem PoissonDeclumping.Bridge.tsum_weight_mul_eq_sigma (μ : PMF ℕ) (F : PlaneTree → ENNReal) : ∑' (T : PlaneTree), PlaneTree.weight μ T * F T = ∑' (d : ℕ) (f : Fin d → PlaneTree), (μ d * ∏ i : Fin d, PlaneTree.weight μ (f i)) * F (PlaneTree.node (List.ofFn f))

Decomposition of ∑_T w(T) F(T) according to the root degree and the children.

theorem PoissonDeclumping.Bridge.tsum_pi_succAbove (d : ℕ) (i : Fin (d + 1)) (F : PlaneTree → (Fin d → PlaneTree) → ENNReal) : (∑' (f : Fin (d + 1) → PlaneTree), F (f i) fun (j : Fin d) => f (i.succAbove j)) = ∑' (t : PlaneTree) (g : Fin d → PlaneTree), F t g

Separating the i-th child: for F depending on the i-th tree and the others, ∑_{f : Fin (d+1) → 𝕋} F(f_i, (f_j)_{j ≠ i}) = ∑_t ∑_g F(t, g).

theorem PoissonDeclumping.Bridge.tsum_child_mark (μ : PMF ℕ) (d : ℕ) (i : Fin (d + 1)) (G : PlaneTree → Prop) (Φ : ℕ → ENNReal) : ∑' (f : Fin (d + 1) → PlaneTree), (∏ j : Fin (d + 1), PlaneTree.weight μ (f j)) * ({t : PlaneTree | G t}.indicator 1 (f i) * Φ (1 + ∑ j : Fin (d + 1), (f j).vertexCount)) = ∫⁻ (t : PlaneTree), {t : PlaneTree | G t}.indicator (fun (t : PlaneTree) => ∑' (q : ℕ), PlaneTree.forestSizeWeight μ d q * Φ (1 + t.vertexCount + q)) t ∂PlaneTree.bienayme μ

Branching property at a marked child (source lines 2236–2240, 2247–2251): for the i-th child among d + 1, ∑_f ∏_j w(f_j) 1{G(f_i)} Φ(1 + ∑_j |f_j|) = E[1{G(𝒯)} ∑_q P(|𝒢_d| = q) Φ(1 + |𝒯| + q)]: the other d children form an independent forest.

theorem PoissonDeclumping.Bridge.lintegral_declumped_le (μ : PMF ℕ) (B : Set ℕ) (G : PlaneTree → Prop) (Φ : ℕ → ENNReal) : ∫⁻ (T : PlaneTree), {T : PlaneTree | PlaneTree.declumpedMark B G T}.indicator (fun (T : PlaneTree) => Φ T.vertexCount) T ∂PlaneTree.bienayme μ ≤ ∑' (d : ℕ), B.indicator (fun (d : ℕ) => ↑d * μ d * ∫⁻ (t : PlaneTree), {t : PlaneTree | G t}.indicator (fun (t : PlaneTree) => ∑' (q : ℕ), PlaneTree.forestSizeWeight μ (d - 1) q * Φ (1 + t.vertexCount + q)) t ∂PlaneTree.bienayme μ) d

The declumped mark and its marked children (source lines 2236–2241, union bound over the marked child): E[1{Ghat(𝒯)} Φ(|𝒯|)] ≤ ∑_{d ∈ B} d μ_d E[1{G(𝒯)} ∑_q P(|𝒢_{d-1}| = q) Φ(1 + |𝒯| + q)].

theorem PoissonDeclumping.Bridge.lintegral_indicator_eq_mul_lintegral_cond (ν : MeasureTheory.Measure PlaneTree) [MeasureTheory.IsFiniteMeasure ν] (s : Set PlaneTree) (f : PlaneTree → ENNReal) : ∫⁻ (t : PlaneTree), s.indicator f t ∂ν = ν s * ∫⁻ (t : PlaneTree), f t ∂ν[|s]

∫⁻ 1_s f dν = ν(s) ∫⁻ f dν(· | s) for a finite measure on plane trees.

theorem PoissonDeclumping.Bridge.lintegral_declumped_le_of_bound (μ : PMF ℕ) (B : Set ℕ) (G : PlaneTree → Prop) (Φ : ℕ → ENNReal) (A : PlaneTree → ENNReal) (κ : ℕ → ENNReal) (hb : ∀ (d : ℕ) (t : PlaneTree), 1 ≤ d → G t → ∑' (q : ℕ), PlaneTree.forestSizeWeight μ (d - 1) q * Φ (1 + t.vertexCount + q) ≤ A t + κ d) : ∫⁻ (T : PlaneTree), {T : PlaneTree | PlaneTree.declumpedMark B G T}.indicator (fun (T : PlaneTree) => Φ T.vertexCount) T ∂PlaneTree.bienayme μ ≤ (PlaneTree.bienayme μ) {T : PlaneTree | G T} * (cB μ B * ∫⁻ (t : PlaneTree), A t ∂(PlaneTree.bienayme μ)[|{T : PlaneTree | G T}] + ∑' (d : ℕ), B.indicator (fun (d : ℕ) => ↑d * μ d * κ d) d)

Union bound over the marked child, with a pointwise forest bound (source lines 2236–2241, 2247–2270): if for every d ≥ 1 and every marked t, ∑_q P(|𝒢_{d-1}| = q) Φ(1 + |t| + q) ≤ A(t) + κ(d), then E[1{Ghat(𝒯)} Φ(|𝒯|)] ≤ π (c_B E[A(𝒯) | G(𝒯) = 1] + ∑_{d ∈ B} d μ_d κ(d)).

Forest convolution and the min(1, D / a_{M_n}) domination

theorem PoissonDeclumping.Bridge.tsum_forestSizeWeight_mul_walkProb (μ : PMF ℕ) (ℓ : ℕ) (N : ℤ) : ∑' (q : ℕ), PlaneTree.forestSizeWeight μ ℓ q * ENNReal.ofReal (walkProb μ (N - ↑q) 0) = ENNReal.ofReal (walkProb μ N (-↑ℓ))

Forest first-passage decomposition, tsum form (source lines 2250–2255, eq:parent_convolution): for every N : ℤ, ∑_q P(|𝒢_ℓ| = q) Ψ_{N-q}(0) = Ψ_N(-ℓ) (both sides vanish for N < 0).

theorem PoissonDeclumping.Bridge.tendsto_tsum_min_div {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) (B : Set ℕ) {l : Filter ℕ} {m : ℕ → ℕ} (hm : Filter.Tendsto m l Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => ∑' (d : ℕ), B.indicator (fun (d : ℕ) => ↑d * LeafHeight.mass μ d * min 1 (↑d / a (m n))) d) l (nhds 0)

The dominated-convergence step of source lines 2242–2245: ∑_{d ∈ B} d μ_d min(1, d / a_{m_n}) → 0 whenever m_n → ∞.

theorem PoissonDeclumping.Bridge.min_le_mul_min_one {u₁ u₂ K y : ℝ} (h1 : u₁ ≤ K) (h2 : u₂ ≤ K * y) : min u₁ u₂ ≤ K * min 1 y

min u₁ u₂ ≤ K min(1, y) when u₁ ≤ K and u₂ ≤ K y.

theorem PoissonDeclumping.Bridge.le_ofReal_min {y : ENNReal} {u v : ℝ} (h1 : y ≤ ENNReal.ofReal u) (h2 : y ≤ ENNReal.ofReal v) : y ≤ ENNReal.ofReal (min u v)

theorem PoissonDeclumping.Bridge.forest_bound_unweighted {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (M : ℕ), 8 ≤ M → ∀ (d : ℕ) (t : PlaneTree), 1 ≤ d → ∑' (q : ℕ), PlaneTree.forestSizeWeight μ (d - 1) q * {s : ℕ | M < s}.indicator 1 (1 + t.vertexCount + q) ≤ {t : PlaneTree | ↑M / 4 < ↑t.vertexCount}.indicator 1 t + ENNReal.ofReal (K * min 1 (↑d / a (M / 2)))

Unweighted forest bound at a marked child (source lines 2236–2245): for M ≥ 8, d ≥ 1 and every tree t, P(1 + |t| + |𝒢_{d-1}| > M) ≤ 1{|t| > M/4} + K min(1, d / a_{⌊M/2⌋}): if |t| ≤ M/4 the other forest has more than M/2 vertices.

theorem PoissonDeclumping.Bridge.forest_bound_weighted {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M n : ℕ), 8 ≤ M → 2 * M ≤ n → ∀ (d : ℕ) (t : PlaneTree), 1 ≤ d → ∑' (q : ℕ), PlaneTree.forestSizeWeight μ (d - 1) q * ENNReal.ofReal ({s : ℕ | M < s}.indicator (fun (s : ℕ) => walkProb μ (↑n - ↑s) 0) (1 + t.vertexCount + q)) ≤ ENNReal.ofReal ({t : PlaneTree | ↑M / 4 < ↑t.vertexCount}.indicator (fun (t : PlaneTree) => supWalk μ (↑n - 1 - ↑t.vertexCount)) t) + ENNReal.ofReal (K / a n * min 1 (↑d / a (M / 2)))

Bridge-weighted forest bound at a marked child (source lines 2247–2264, eq:parent_convolution, eq:parent_forest, numerator form): for M ≥ 8, n ≥ 2M, d ≥ 1 and every tree t, E[Ψ_{n-1-|t|-|𝒢_{d-1}|}(0) 1{1 + |t| + |𝒢_{d-1}| > M}] ≤ 1{|t| > M/4} sup_x Ψ_{n-1-|t|}(x) + (K / a_n) min(1, d / a_{⌊M/2⌋}). The first term is the convolution bound, the second combines it with the weighted forest tail (the other forest has more than M/2 vertices).

Lemma lem:root_declumping(iii)

theorem PoissonDeclumping.Bridge.tsum_indicator_mul_ofReal_min {μ : PMF ℕ} (hc : IsCritical μ) (B : Set ℕ) {K x : ℝ} (hK : 0 ≤ K) (hx : 0 < x) : ∑' (d : ℕ), B.indicator (fun (d : ℕ) => ↑d * μ d * ENNReal.ofReal (K * min 1 (↑d / x))) d = ENNReal.ofReal (K * ∑' (d : ℕ), B.indicator (fun (d : ℕ) => ↑d * LeafHeight.mass μ d * min 1 (↑d / x)) d)

∑_{d ∈ B} d μ_d K min(1, d / x) = K ∑_{d ∈ B} d μ_d min(1, d / x) (from ℝ≥0∞ to ℝ).

theorem PoissonDeclumping.Bridge.toReal_le_mul_add {Y P C X : ENNReal} {y : ℝ} (hP : P ≠ ⊤) (hC : C ≠ ⊤) (hX : X ≠ ⊤) (hy : 0 ≤ y) (h : Y ≤ P * (C * X + ENNReal.ofReal y)) : Y.toReal ≤ P.toReal * (C.toReal * X.toReal + y)

From Y ≤ P (C X + y) in ℝ≥0∞ to ℝ.

theorem PoissonDeclumping.Bridge.indicator_indicator_vertexCount {β : Type u_1} [Zero β] (S : Set PlaneTree) (P : ℕ → Prop) (f : ℕ → β) (T : PlaneTree) : S.indicator (fun (T : PlaneTree) => {s : ℕ | P s}.indicator f T.vertexCount) T = {T : PlaneTree | T ∈ S ∧ P T.vertexCount}.indicator (fun (T : PlaneTree) => f T.vertexCount) T

theorem PoissonDeclumping.Bridge.tsum_indicator_min_nonneg {μ : PMF ℕ} (B : Set ℕ) (x : ℝ) (hx : 0 ≤ x) : 0 ≤ ∑' (d : ℕ), B.indicator (fun (d : ℕ) => ↑d * LeafHeight.mass μ d * min 1 (↑d / x)) d

theorem PoissonDeclumping.Bridge.microscopic_declumped {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} {B : Set ℕ} (hS : StructuralMicroscopic μ a G k M) (hM : IsCutoff M) (hB0 : 0 < cB μ B) (hB1 : cB μ B < ⊤) : Microscopic μ (fun (j : ℕ) => PlaneTree.declumpedMark B (G j)) k M

Lemma lem:root_declumping(iii) (source lines 2212–2214, 2231–2298, P16): if the raw marks (G_k) satisfy Assumption (S) along (k_n) with respect to the cutoff (M_n) and c_B ∈ (0, ∞), then the declumped marks Ghat_k = declumpedMark B G_k satisfy Assumption (M) along (k_n) with respect to the same cutoff. Periodic offspring laws are included: the paper's "replace n by n - 1" (line 2286) is replaced by the numerator form of Lemma lem:consequenceM with time shift j = 1 (consequenceM_weighted_sup), so no Ψ_{n-1}(-1) appears (correction F3).