Elementary criteria used in the applications (Sections 6–7)

• eventually_mul_add_le_rpow: if f_n ≤ n^{o(1)} (in the form: for every δ > 0, eventually f_n ≤ n^δ), then also C f_n + D ≤ n^{o(1)}. This is how the hypotheses "s_{r,k_n} + ℓ_{r,k_n} = n^{o(1)}", "k_n = n^{o(1)}", "κ^{k_n} = n^{o(1)}" of Lemmas lem:S_rary and lem:S_lh (source lines 2644–2653, 3053–3064) are transported to the moment bound E_{k_n}[C_{k_n} + L_{k_n}] = n^{o(1)} required by Lemma lem:critM.
• nonClustering_of_pairSum_le: the final step of the proofs of Lemmas lem:S_rary(ii), lem:C_rary and lem:C_lh (source lines 2750–2753, 2787–2791, 3234–3236): a summed pair bound ∑_{ℓ=1}^{M_n} A_n(ℓ) ≤ K π_n + C M_n π_n² gives Assumption (C) as soon as M_n = o(n) and K π_n = o(n π_n²) (e.g. K = 0, or n π_n → ∞).

theorem PoissonDeclumping.eventually_mul_add_le_rpow {l : Filter ℕ} (hl : l ≤ Filter.atTop) {f : ℕ → ℝ} (hf : ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in l, f n ≤ ↑n ^ δ) {C : ℝ} (hC : 0 ≤ C) (D δ : ℝ) : 0 < δ → ∀ᶠ (n : ℕ) in l, C * f n + D ≤ ↑n ^ δ

If f_n ≤ n^δ eventually for every δ > 0, then the same holds for C f_n + D (C ≥ 0), along any filter finer than atTop.

theorem PoissonDeclumping.cond_univ_le_one {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] (s : Set α) : ν[Set.univ | s] ≤ 1

A conditional measure has total mass at most one (it is 0 when the conditioning event is null).

theorem PoissonDeclumping.pairProb_nonneg (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (n ℓ : ℕ) : 0 ≤ pairProb μ G k n ℓ

theorem PoissonDeclumping.nonClustering_of_pairSum_le {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : (fun (n : ℕ) => ↑(M n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {K C : ℝ} (hC : 0 ≤ C) (hK : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in admissibleSizes μ, K * markProb μ G k n ≤ ε * (↑n * markProb μ G k n ^ 2)) (h : ∀ (n : ℕ), ∑ ℓ ∈ Finset.Icc 1 (M n), pairProb μ G k n ℓ ≤ K * markProb μ G k n + C * ↑(M n) * markProb μ G k n ^ 2) : NonClustering μ G k M

A summed pair bound ∑_{ℓ=1}^{M_n} A_n(ℓ) ≤ K π_n + C M_n π_n² gives Assumption (C) when M_n = o(n) and K π_n = o(n π_n²) along admissible sizes.

theorem PoissonDeclumping.eventually_mul_le_of_tendsto {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k : ℕ → ℕ} (hπ : Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ G k n) (admissibleSizes μ) Filter.atTop) (K ε : ℝ) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in admissibleSizes μ, K * markProb μ G k n ≤ ε * (↑n * markProb μ G k n ^ 2)

The condition K π_n = o(n π_n²) of nonClustering_of_pairSum_le holds when n π_n → ∞.