Statement-level definitions

Every definition on which the statements of the four Introduction theorems depend: finite plane trees, fringe subtrees and marked counts, Bienaymé laws and size conditioning, total variation, the Łukasiewicz walk and hypothesis (H_α), cutoffs and Assumptions (M), (S), (C), and the four statement propositions (PoissonApproximationStatement, PoissonApproximation2Statement, MaxStringStatement, MaxLeafHeightStatement), proved in PoissonDeclumping.MainTheorems.

These definitions originate in the upstream statement contract. The phase refinement in TwoPointLocalization is strengthened here to every nontrivial filter of admissible sizes, so that it applies to phase-separated subsequences even when the full sequence approaches integer phases. The remaining definitions retain the upstream statements.

Plane trees and fringe subtrees (lemmas: PlaneTree/Basic.lean)

inductive PoissonDeclumping.PlaneTree : Type

A finite plane tree consists of a root and an ordered list of child trees.

• node (children : List PlaneTree) : PlaneTree

def PoissonDeclumping.PlaneTree.children : PlaneTree → List PlaneTree

Ordered child subtrees of the root. A leaf has an empty list of children.

Equations

• (PoissonDeclumping.PlaneTree.node ts).children = ts

def PoissonDeclumping.PlaneTree.rootDegree (T : PlaneTree) : ℕ

Outdegree of the root.

Equations

• T.rootDegree = T.children.length

@[irreducible]

def PoissonDeclumping.PlaneTree.fringeTrees : PlaneTree → List PlaneTree

One fringe subtree per vertex, in depth-first order, including the root.

Equations

• (PoissonDeclumping.PlaneTree.node ts).fringeTrees = PoissonDeclumping.PlaneTree.node ts :: List.flatMap PoissonDeclumping.PlaneTree.fringeTrees ts

def PoissonDeclumping.PlaneTree.vertexCount (T : PlaneTree) : ℕ

Number of vertices, including the root.

Equations

• T.vertexCount = T.fringeTrees.length

noncomputable def PoissonDeclumping.PlaneTree.markCount (G : PlaneTree → Prop) (T : PlaneTree) : ℕ

Number of vertices whose fringe subtree satisfies the marking predicate.

Equations

• PoissonDeclumping.PlaneTree.markCount G T = List.countP (fun (U : PoissonDeclumping.PlaneTree) => decide (G U)) T.fringeTrees

def PoissonDeclumping.PlaneTree.declumpedMark (B : Set ℕ) (G : PlaneTree → Prop) (T : PlaneTree) : Prop

The declumped mark of Section 1.2: an allowed root degree and a marked child.

Equations

• PoissonDeclumping.PlaneTree.declumpedMark B G T = (T.rootDegree ∈ B ∧ ∃ U ∈ T.children, G U)

Discrete σ-algebra, outdegree sequence (lemmas: PlaneTree/Countable.lean)

@[instance_reducible]

instance PoissonDeclumping.PlaneTree.instMeasurableSpace : MeasurableSpace PlaneTree

The discrete σ-algebra: every set of finite plane trees is measurable.

Equations

• PoissonDeclumping.PlaneTree.instMeasurableSpace = ⊤

def PoissonDeclumping.PlaneTree.degSeq (T : PlaneTree) : List ℕ

Outdegrees of the vertices in depth-first order, one entry per vertex (k_{u_1}(T), …, k_{u_n}(T)). The paper's DFS sequence 𝐱(T) is this list shifted by -1.

Equations

• T.degSeq = List.map PoissonDeclumping.PlaneTree.rootDegree T.fringeTrees

Complete r-ary trees, non-fringe embeddings and leaf-height (Sections 1.3–1.4, 2.1)

def PoissonDeclumping.PlaneTree.completeTree (r : ℕ) : ℕ → PlaneTree

The complete r-ary tree H_{r,k} of height k: all leaves at distance k from the root, every internal vertex with exactly r children.

Equations

• PoissonDeclumping.PlaneTree.completeTree r 0 = PoissonDeclumping.PlaneTree.node []
• PoissonDeclumping.PlaneTree.completeTree r k.succ = PoissonDeclumping.PlaneTree.node (List.replicate r (PoissonDeclumping.PlaneTree.completeTree r k))

inductive PoissonDeclumping.PlaneTree.Embeds : PlaneTree → PlaneTree → Prop

Embeds T' T is the paper's T' ≺ T: T is obtained from T' by grafting plane trees onto the leaves of T'. A leaf of T' matches an arbitrary tree; a vertex of T' with d ≥ 1 children matches a vertex of T with exactly d children, whose children are matched in order.

• leaf (T : PlaneTree) : (PlaneTree.node []).Embeds T
• node (cs ts : List PlaneTree) (hne : cs ≠ []) (hlen : cs.length = ts.length) (h : ∀ (i : ℕ) (hi : i < cs.length), cs[i].Embeds ts[i]) : (PlaneTree.node cs).Embeds (PlaneTree.node ts)

noncomputable def PoissonDeclumping.PlaneTree.maxCompleteHeight (r : ℕ) (T : PlaneTree) : ℕ

H_r(T) = max {k ≥ 0 : ∃ u ∈ T, H_{r,k} ≺ T_u}; the set is nonempty (it contains 0) and, for r ≥ 1, bounded by the number of vertices.

Equations

• PoissonDeclumping.PlaneTree.maxCompleteHeight r T = sSup {k : ℕ | ∃ U ∈ T.fringeTrees, (PoissonDeclumping.PlaneTree.completeTree r k).Embeds U}

@[irreducible]

def PoissonDeclumping.PlaneTree.rootLeafHeight : PlaneTree → ℕ

The leaf-height λ_∅(T) of the root: the number of edges to the closest leaf descendant (0 for a leaf, 1 + the minimum over the children otherwise).

Equations

• (PoissonDeclumping.PlaneTree.node []).rootLeafHeight = 0
• (PoissonDeclumping.PlaneTree.node (t :: us)).rootLeafHeight = List.foldr min t.rootLeafHeight (List.map PoissonDeclumping.PlaneTree.rootLeafHeight us) + 1

def PoissonDeclumping.PlaneTree.leafHeight (T : PlaneTree) : ℕ

The leaf-height λ(T) = max_{v ∈ T} λ_v(T) of a tree.

Equations

• T.leafHeight = List.foldr max 0 (List.map PoissonDeclumping.PlaneTree.rootLeafHeight T.fringeTrees)

Bienaymé trees and size conditioning (Section 2.1)

def PoissonDeclumping.IsCritical (μ : PMF ℕ) : Prop

μ is critical: its mean ∑ j μ_j equals one. The sum is taken in ℝ≥0∞, so this statement includes finiteness of the mean.

Equations

• PoissonDeclumping.IsCritical μ = (∑' (j : ℕ), ↑j * μ j = 1)

noncomputable def PoissonDeclumping.PlaneTree.weight (μ : PMF ℕ) (T : PlaneTree) : ENNReal

The Bienaymé weight ∏_{u∈T} μ_{k_u(T)} of a finite plane tree: the product of the offspring masses of the outdegrees of its vertices, listed in depth-first order.

Equations

• PoissonDeclumping.PlaneTree.weight μ T = (List.map (⇑μ) T.degSeq).prod

noncomputable def PoissonDeclumping.PlaneTree.bienayme (μ : PMF ℕ) : MeasureTheory.Measure PlaneTree

The law of a μ-Bienaymé tree, as a measure on finite plane trees (with the discrete σ-algebra). It is a probability measure for critical μ with μ 1 ≠ 1 (PoissonDeclumping.PlaneTree.bienayme_isProbabilityMeasure).

Equations

• PoissonDeclumping.PlaneTree.bienayme μ = MeasureTheory.Measure.sum fun (T : PoissonDeclumping.PlaneTree) => PoissonDeclumping.PlaneTree.weight μ T • MeasureTheory.Measure.dirac T

def PoissonDeclumping.PlaneTree.Admissible (μ : PMF ℕ) (n : ℕ) : Prop

A size n is admissible if a μ-Bienaymé tree has n vertices with positive probability.

Equations

• PoissonDeclumping.PlaneTree.Admissible μ n = (0 < (PoissonDeclumping.PlaneTree.bienayme μ) {T : PoissonDeclumping.PlaneTree | T.vertexCount = n})

noncomputable def PoissonDeclumping.PlaneTree.conditioned (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure PlaneTree

The μ-Bienaymé tree conditioned to have n vertices. This is a probability measure exactly at admissible n (and the zero measure otherwise).

Equations

• PoissonDeclumping.PlaneTree.conditioned μ n = (PoissonDeclumping.PlaneTree.bienayme μ)[|{T : PoissonDeclumping.PlaneTree | T.vertexCount = n}]

Total variation (lemmas: Probability/TotalVariation.lean)

noncomputable def PoissonDeclumping.paperTVDist {α : Type u_1} [MeasurableSpace α] (μ ν : MeasureTheory.Measure α) : ℝ

Total variation in the paper's probability convention. For finite measures this is half of mathlib's total variation. Like mathlib's real-valued distance, it is totalized to zero if either measure is infinite; probabilistic uses must retain their probability-measure hypotheses.

Equations

• PoissonDeclumping.paperTVDist μ ν = MeasureTheory.tvDist μ ν / 2

The Łukasiewicz walk and the stable-domain hypothesis (H_α)

noncomputable def PoissonDeclumping.stepLaw (μ : PMF ℕ) : MeasureTheory.Measure ℤ

The law of one increment X = K - 1, P(X = i) = μ_{i+1} for i ≥ -1.

Equations

• PoissonDeclumping.stepLaw μ = MeasureTheory.Measure.map (fun (k : ℕ) => ↑k - 1) μ.toMeasure

noncomputable def PoissonDeclumping.walkLaw (μ : PMF ℕ) : ℕ → MeasureTheory.Measure ℤ

The law of the random walk S_m = X_1 + … + X_m (S_0 = 0) as an m-fold convolution.

Equations

• PoissonDeclumping.walkLaw μ 0 = MeasureTheory.Measure.dirac 0
• PoissonDeclumping.walkLaw μ k.succ = (PoissonDeclumping.walkLaw μ k).conv (PoissonDeclumping.stepLaw μ)

def PoissonDeclumping.SlowlyVarying (ℓ : ℝ → ℝ) : Prop

A slowly varying function at infinity: ℓ(a x) / ℓ(x) → 1 for every a > 0 (the paper's literal definition, line 850: no positivity or measurability is required; it is used only on the hypothesis side, where a weaker notion would strengthen the theorems).

Equations

• PoissonDeclumping.SlowlyVarying ℓ = ∀ (a : ℝ), 0 < a → Filter.Tendsto (fun (x : ℝ) => ℓ (a * x) / ℓ x) Filter.atTop (nhds 1)

structure PoissonDeclumping.StableDomain (μ : PMF ℕ) (α : ℝ) (a : ℕ → ℝ) : Prop

Hypothesis (H_α) with normalizing sequence a: μ is critical, μ_1 ≠ 1, α ∈ (1,2], and a is a nondecreasing sequence (the paper's "increasing"), positive for n ≥ 1, for which (K_1+…+K_n−n)/a_n → Y_α in distribution, where Y_α (with law ν) has E exp(-λ Y_α) = exp(λ^α) for all λ > 0. Convergence in distribution is expressed through bounded continuous test functions (equivalent to weak convergence of the laws). No truncated-moment criterion or local-limit estimate is assumed; the latter is proved from this normalized attraction hypothesis.

• critical : IsCritical μ
• nondegenerate : μ 1 ≠ 1
• alpha_mem : 1 < α ∧ α ≤ 2
• monotone : Monotone a
• pos (n : ℕ) : 1 ≤ n → 0 < a n
• converges : ∃ (ν : MeasureTheory.Measure ℝ), MeasureTheory.IsProbabilityMeasure ν ∧ (∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ α)) ∧ ∀ (f : BoundedContinuousFunction ℝ ℝ), Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), f x ∂MeasureTheory.Measure.map (fun (z : ℤ) => ↑z / a n) (walkLaw μ n)) Filter.atTop (nhds (∫ (x : ℝ), f x ∂ν))

def PoissonDeclumping.InStableDomain (μ : PMF ℕ) : Prop

(H_α) for some α and some normalizing sequence (the phrase "critical and belongs to the domain of attraction of a stable law" of Theorems 1.3 and 1.4).

Equations

• PoissonDeclumping.InStableDomain μ = ∃ (α : ℝ) (a : ℕ → ℝ), PoissonDeclumping.StableDomain μ α a

Marks, cutoffs and Assumptions (M), (S), (C)

@[instance_reducible]

instance PoissonDeclumping.instMeasurableSpaceListPlaneTree : MeasurableSpace (List PlaneTree)

Lists of plane trees (a countable type) carry the discrete σ-algebra.

Equations

• PoissonDeclumping.instMeasurableSpaceListPlaneTree = ⊤

def PoissonDeclumping.admissibleSizes (μ : PMF ℕ) : Filter ℕ

Limits are taken along admissible sizes: n → ∞ with P(|𝒯| = n) > 0.

Equations

• PoissonDeclumping.admissibleSizes μ = Filter.atTop ⊓ Filter.principal {n : ℕ | PoissonDeclumping.PlaneTree.Admissible μ n}

structure PoissonDeclumping.IsCutoff (M : ℕ → ℕ) : Prop

A cutoff sequence: positive integers (for n ≥ 1) with M_n → ∞ and M_n = o(n).

• pos (n : ℕ) : 1 ≤ n → 0 < M n
• tendsto_atTop : Filter.Tendsto M Filter.atTop Filter.atTop
• isLittleO : (fun (n : ℕ) => ↑(M n)) =o[Filter.atTop] fun (n : ℕ) => ↑n

noncomputable def PoissonDeclumping.markProb (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (n : ℕ) : ℝ

π_n = P(G_{k_n}(𝒯) = 1) for the unconditioned Bienaymé tree.

Equations

• PoissonDeclumping.markProb μ G k n = (PoissonDeclumping.PlaneTree.bienayme μ).real {T : PoissonDeclumping.PlaneTree | G (k n) T}

noncomputable def PoissonDeclumping.uniformFringeLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure PlaneTree

The law of the fringe subtree 𝒯^n_{U_n} at a uniform vertex U_n of 𝒯^n, with U_n independent of 𝒯^n: sample T ~ 𝒯^n and an independent uniform DFS index i < n, and take the fringe subtree of the i-th vertex.

Equations

• One or more equations did not get rendered due to their size.

def PoissonDeclumping.Microscopic (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k M : ℕ → ℕ) : Prop

Assumption (M), microscopicity: P(G_{k_n}(𝒯^n_{U_n}) = 1) ∼ P(G_{k_n}(𝒯) = 1) and P(|𝒯^n_{U_n}| > M_n | G_{k_n}(𝒯^n_{U_n}) = 1) = o(1). The conditional probability is mathlib's cond, which is 0 when the conditioning event is null (the paper works along subsequences with positive marking probability, line 206).

Equations

• One or more equations did not get rendered due to their size.

structure PoissonDeclumping.Skeleton (μ : PMF ℕ) (G : PlaneTree → Prop) (ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)) : Prop

A decomposition as in Assumption (S) for one mark G, i.e. under P_k = P(· | G(𝒯) = 1). It is a law ρ of (𝒯, C, 𝒯^{(1)},…,𝒯^{(L)}) on PlaneTree × ℕ × List PlaneTree, with L the length of the list, such that: (1) the first coordinate has law P(· | G(𝒯) = 1); (2) conditionally on (C, L) the listed trees are independent with the law of 𝒯 (the product formula for point masses); (3) almost surely |𝒯| = C + ∑_{i ≤ L} |𝒯^{(i)}|. (The paper's infinite sequence 𝒯^{(1)}, 𝒯^{(2)},… only matters through its first L terms.)

• isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure ρ
• law_tree : MeasureTheory.Measure.map Prod.fst ρ = (PlaneTree.bienayme μ)[|{T : PlaneTree | G T}]
• conditionally_iid (c : ℕ) (ts : List PlaneTree) : ρ {ω : PlaneTree × ℕ × List PlaneTree | ω.2.1 = c ∧ ω.2.2 = ts} = ρ {ω : PlaneTree × ℕ × List PlaneTree | ω.2.1 = c ∧ ω.2.2.length = ts.length} * (List.map (PlaneTree.weight μ) ts).prod
• size_eq : ∀ᵐ (ω : PlaneTree × ℕ × List PlaneTree) ∂ρ, ω.1.vertexCount = ω.2.1 + (List.map PlaneTree.vertexCount ω.2.2).sum

def PoissonDeclumping.StructuralMicroscopic (μ : PMF ℕ) (a : ℕ → ℝ) (G : ℕ → PlaneTree → Prop) (k M : ℕ → ℕ) : Prop

Assumption (S), structural microscopicity, with respect to the normalizing sequence a of (H_α): for each mark G_k with P(G_k(𝒯) = 1) > 0 there is a decomposition ρ_k (the paper works along subsequences with positive marking probability, line 206; at null marks ρ_k is unconstrained), and for every ε > 0 a_n P_{k_n}(C_{k_n} > ε M_n) → 0 and E_{k_n}[L_{k_n}] / a_{M_n} → 0.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PoissonDeclumping.pairProb (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (n ℓ : ℕ) : ℝ

A_n(ℓ) = P(|𝒯| ≥ ℓ+1, G_{k_n}(𝒯) = 1, G_{k_n}(𝒯_{u_{ℓ+1}}) = 1); the (ℓ+1)-st vertex in DFS order has fringe tree T.fringeTrees[ℓ].

Equations

• PoissonDeclumping.pairProb μ G k n ℓ = (PoissonDeclumping.PlaneTree.bienayme μ).real {T : PoissonDeclumping.PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ G (k n) T ∧ ∃ U ∈ T.fringeTrees[ℓ]?, G (k n) U}

def PoissonDeclumping.NonClustering (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k M : ℕ → ℕ) : Prop

Assumption (C), pair non-clustering: ∑_{ℓ=1}^{M_n} A_n(ℓ) = o(n π_n²).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PoissonDeclumping.markedCountLaw (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (n : ℕ) : MeasureTheory.Measure ℕ

The number of marked fringe subtrees #{u ∈ 𝒯^n : G_{k_n}(𝒯^n_u) = 1} is markCount (G (k n)), a random variable on conditioned μ n. Its law, as a measure on ℕ.

Equations

• PoissonDeclumping.markedCountLaw μ G k n = MeasureTheory.Measure.map (PoissonDeclumping.PlaneTree.markCount (G (k n))) (PoissonDeclumping.PlaneTree.conditioned μ n)

Statements of the four Introduction theorems

def PoissonDeclumping.PoissonApproximationStatement : Prop

Theorem 1.1 (thm:PoissonApproximation, source lines 305–329).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PoissonDeclumping.cB (μ : PMF ℕ) (B : Set ℕ) : ENNReal

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

Equations

• PoissonDeclumping.cB μ B = ∑' (j : ℕ), B.indicator (fun (j : ℕ) => ↑j * μ j) j

def PoissonDeclumping.PoissonApproximation2Statement : Prop

Theorem 1.2 (thm:PoissonApproximation2, source lines 396–442): root declumping. The raw marks satisfy (S) and the declumped marks Ghat_k = declumpedMark B G_k satisfy (C), both with the same cutoff sequence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PoissonDeclumping.tStar (μ₁ : ℝ) (n : ℕ) : ℝ

The centering t_n^* of Theorem 1.3(i).

Equations

• PoissonDeclumping.tStar μ₁ n = (Real.log ↑n + Real.log (1 - μ₁)) / Real.log (1 / μ₁)

noncomputable def PoissonDeclumping.tStarStar (r : ℕ) (μᵣ : ℝ) (n : ℕ) : ℝ

The centering t_n^{**} of Theorem 1.3(ii).

Equations

• PoissonDeclumping.tStarStar r μᵣ n = Real.logb (↑r) (Real.log ↑n) - Real.logb (↑r) (Real.log (1 / μᵣ) / (↑r - 1))

def PoissonDeclumping.twoPointSet (x : ℝ) : Set ℤ

The two-point set J_n: {m_n - 1, m_n} if θ_n ≤ 1/2, otherwise {m_n, m_n + 1}, where m_n = ⌊x⌋ and θ_n = {x} for the centering x.

Equations

• PoissonDeclumping.twoPointSet x = if Int.fract x ≤ 1 / 2 then {⌊x⌋ - 1, ⌊x⌋} else {⌊x⌋, ⌊x⌋ + 1}

def PoissonDeclumping.TwoPointLocalization (μ : PMF ℕ) (H : PlaneTree → ℕ) (x : ℕ → ℝ) : Prop

Localization on J_n along all admissible sizes, and on m_n along every nontrivial filter of admissible sizes whose phases stay a positive distance from the integers. In particular, the single-point refinement applies to every such admissible subsequence.

Equations

• One or more equations did not get rendered due to their size.

def PoissonDeclumping.LatticeGumbel (μ : PMF ℕ) (H : PlaneTree → ℕ) (μ₁ : ℝ) (x : ℕ → ℝ) : Prop

The lattice-modulated Gumbel limit P(H(𝒯^n) ≤ ⌊x_n + t⌋) − exp(−μ₁^{t+1−{x_n+t}}) → 0 for every real t.

Equations

• One or more equations did not get rendered due to their size.

def PoissonDeclumping.MaxStringStatement : Prop

Theorem 1.3 (thm:max_string, source lines 475–501): the maximal complete non-fringe r-ary height H_r = maxCompleteHeight r.

Equations

• One or more equations did not get rendered due to their size.

def PoissonDeclumping.MaxLeafHeightStatement : Prop

Theorem 1.4 (thm:max_lh, source lines 533–558): the maximum leaf-height λ = PlaneTree.leafHeight. The constants C_μ, D_μ are identified with the limits of the root leaf-height tails π_k = P(λ_∅(𝒯) ≥ k) (source lines 562–572), as the paper records; the centerings are k_n^* and k_n^{**}.

Equations

• One or more equations did not get rendered due to their size.