The random-walk toolkit

Source lines 837–883 ("Random walk toolbox"), inventory B06–B10, B14.

The bridge estimates of Sections 3–5 of the paper (forest estimates, microscopicity, bridge removal, truncation, the Chen–Stein error terms, Theorems 1.1 and 1.2) use only a handful of facts about the Łukasiewicz walk S_m = X_1 + ⋯ + X_m (Ψ_m(x) = walkProb μ m x) and its normalizing sequence a. StableToolkit μ α a collects exactly these facts, stated as honest inequalities and limits about walkProb, walkLaw and a. The bridge lemmas of Sections 3–5 take this structure as their hypothesis; it is derived from the paper's standing assumption by

PoissonDeclumping.Stable.stableToolkit : StableDomain μ α a → StableToolkit μ α a

(Stable/ToolkitProof.lean), so the final theorems (MainTheorems.lean) assume only (H_α). No field states a conclusion of a paper lemma; each field is a direct consequence of the (lattice) local limit theorem, of tightness of S_m / a_m, or of regular variation of a.

Periodic offspring laws

Periodic laws are not excluded. With d = gcd {i - j : μ_i μ_j > 0} (the span; μ_0 > 0 for critical μ ≠ δ_1, so every step is ≡ -1 (mod d)), S_m ∈ -m + dℤ almost surely and the lattice local limit theorem (source lines 867–876) reads sup_{x ∈ -m + dℤ} |a_m Ψ_m(x) - d · p_α(x / a_m)| → 0, where p_α is the density of Y_α. The stable density is not introduced: LatticeLocal μ a d L records only the three consequences that the proofs use, with L = d · p_α(0) > 0:

• support: Ψ_m(x) ≠ 0 → d ∣ x + m (compatible endpoints);
• origin: a_n Ψ_n(x) → L uniformly over compatible |x| ≤ η a_n (continuity of p_α at 0 and p_α(0) > 0);
• equicont: |a_n Ψ_n(x) - a_n Ψ_n(y)| is small uniformly over compatible x, y with |x - y| ≤ η a_n (uniform continuity of p_α).

Every uniform statement is restricted to compatible lattice points, so no conditional law at a zero-probability endpoint is ever used.

Consequences proved here (from the fields only)

• StableToolkit.rho_pos, rho_lt_one, tendsto_atTop: 0 < 1/α < 1, a_n → ∞.
• StableToolkit.exists_le_div_of_le_two_mul: Ψ_m(x) ≤ C / a_n whenever n ≤ 2m.
• StableToolkit.exists_eventually_le_sub: a_{t-j} ≥ (1 - ε) a_t for j ≤ δ t.
• StableToolkit.eventually_abs_mul_sub_le, eventually_bounds, eventually_abs_div_sub_one_le: for total lengths N_n → ∞, m_n = o(N_n) and z_n = o(a_{N_n}), a_{N_n} Ψ_{N_n-j}(x) → L and Ψ_{N_n-j}(x) / Ψ_{N_n}(y) → 1 uniformly over j ≤ m_n and compatible |x|, |y| ≤ z_n (the "ratio → 1" step of source lines 965, 1033, 1236, 1293, 1752, 2067, 2293, and the lower bounds of lines 1647, 1958, 1981).
• StableToolkit.exists_lower_bound_neg_one: Ψ_n(-1) ≥ c / a_n for every n ≥ 1 with Ψ_n(-1) > 0, i.e. at every admissible size (Dwass), with one constant c.
• StableToolkit.eventually_walkProb_neg_one_pos_iff: for large n, Ψ_n(-1) > 0 ↔ d ∣ n - 1 (in the aperiodic case d = 1 all large n are admissible).
• StableToolkit.eventually_walkLaw_tail_le: if r_n / a_{M_n} → ∞ then max_{i ≤ M_n} P(|S_i| > r_n) → 0 (the only use of "maximal tightness", lines 1763–1770, 1912; marginal uniform tightness suffices).
• isProbabilityMeasure_walkLaw: each walkLaw μ m is a probability measure, supplied by the common instances in Setup/Walk.lean.

structure PoissonDeclumping.LatticeLocal (μ : PMF ℕ) (a : ℕ → ℝ) (d : ℕ) (L : ℝ) : Prop

The lattice local limit theorem, without the stable density (source lines 860–883, inventory B09). d is the span of the walk (S_m ∈ -m + dℤ a.s.) and L = d · p_α(0) with p_α the density of Y_α.

• support (lines 876–879): outside the lattice -m + dℤ the probability is zero. Used to show that the endpoints met in the proofs are compatible: P(|𝒯| = m) > 0 → d ∣ m - 1 (via Dwass), S_M ∈ -M + dℤ, hence 0 is compatible with n - |𝒯| and -1 - S_M with n - M at admissible n (lines 965, 1033, 1293, 1752, 2067, 2293).
• origin (eq:LL plus continuity and positivity of p_α at 0): a_n Ψ_n(x) → L uniformly over compatible |x| ≤ η a_n. Used for every lower bound Ψ_n(k) ≥ c / a_n (lines 1034, 1164, 1231, 1329, 1647, 1774, 1981, 2069) and every ratio limit Ψ_{n-m}(x) / Ψ_n(-1) → 1 (lines 965, 1033, 1236, 1293, 1752, 2067, 2293).
• equicont (eq:LL plus uniform continuity of p_α): replaces the Skorokhod/dominated convergence endpoint smoothing in the proof of eq:approx3 (lines 1968–1994, B14); the smoothing becomes a deterministic uniform bound.

• d_pos : 0 < d
• L_pos : 0 < L
• support (m : ℕ) (x : ℤ) : walkProb μ (↑m) x ≠ 0 → ↑d ∣ x + ↑m
• origin (ε : ℝ) : 0 < ε → ∃ (η : ℝ), 0 < η ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (x : ℤ), ↑d ∣ x + ↑n → |↑x| ≤ η * a n → |a n * walkProb μ (↑n) x - L| ≤ ε
• equicont (ε : ℝ) : 0 < ε → ∃ (η : ℝ), 0 < η ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (x y : ℤ), ↑d ∣ x + ↑n → ↑d ∣ y + ↑n → |↑(x - y)| ≤ η * a n → |a n * walkProb μ (↑n) x - a n * walkProb μ (↑n) y| ≤ ε

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

The random-walk toolkit used by the bridge estimates of Sections 3–5 (source lines 837–883). A temporary conditional interface: it must be derived from StableDomain μ α a.

• critical, nondegenerate, alpha_mem: the standing hypotheses (H_α) (lines 705–712), copied from StableDomain so that bridge lemmas need a single hypothesis.
• monotone, pos, regularlyVarying (lines 846–853, B06/B08): a is increasing, positive, regularly varying of index 1/α. Potter bounds, a_{M_n}/a_n → 0, a_{n-o(n)}/a_n → 1, a_n = o(n), a_n = n^{1/α+o(1)} and Karamata's sums are theorems of PoissonDeclumping.RegularVariation.* and are not fields. Used at lines 1087–1105, 1145–1177, 1218, 1346–1348, 1752, 1896, 1958, 1986, 2244.
• sup_le (local bound "following from eq:LL", B10): Ψ_m(x) ≤ C / a_m for all m ≥ 1 and all x. Used at lines 1034, 1140, 1161, 1176, 1340, 1647, 1774, 1983, 2069, 2254.
• tight (B07, only in its marginal form): S_m / a_m is tight, uniformly in m ≥ 1. The paper invokes functional convergence (eq:cvlaw) for max_{i ≤ M_n} P(|S_i| > r_n - 1) → 0 (lines 1763–1770) and convergence in law of S_{M_n}/a_{M_n} (line 1912); both only need this. Used through eventually_walkLaw_tail_le.
• lattice: the lattice local limit theorem, see LatticeLocal.

• critical : IsCritical μ
• nondegenerate : μ 1 ≠ 1
• alpha_mem : 1 < α ∧ α ≤ 2
• monotone : Monotone a
• pos (n : ℕ) : 1 ≤ n → 0 < a n
• regularlyVarying : RegularlyVaryingSeq (1 / α) a
• sup_le : ∃ (C : ℝ), ∀ (m : ℕ), 1 ≤ m → ∀ (x : ℤ), walkProb μ (↑m) x ≤ C / a m
• tight (ε : ℝ) : 0 < ε → ∃ (K : ℝ), ∀ (m : ℕ), 1 ≤ m → (walkLaw μ m).real {x : ℤ | K * a m < |↑x|} ≤ ε
• lattice : ∃ (d : ℕ) (L : ℝ), LatticeLocal μ a d L

theorem PoissonDeclumping.walkProb_natCast_real (μ : PMF ℕ) (m : ℕ) (x : ℤ) : walkProb μ (↑m) x = (walkLaw μ m).real {x}

Ψ_m(x) = P(S_m = x) at a natural time.

theorem PoissonDeclumping.StableToolkit.rho_pos {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : 0 < 1 / α

theorem PoissonDeclumping.StableToolkit.rho_lt_one {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : 1 / α < 1

theorem PoissonDeclumping.StableToolkit.tendsto_atTop {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : Filter.Tendsto a Filter.atTop Filter.atTop

a_n → ∞.

theorem PoissonDeclumping.StableToolkit.exists_le_div_of_le_two_mul {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n m : ℕ), 1 ≤ n → 1 ≤ m → n ≤ 2 * m → ∀ (x : ℤ), walkProb μ (↑m) x ≤ C / a n

The local bound at comparable times: Ψ_m(x) ≤ C / a_n whenever n ≤ 2m (lines 1161–1164, 1340, 1647, 1774, 2069: Ψ_{n-q}, Ψ_{n-c}, Ψ_{n-m_n}, Ψ_{n-2M_n} are O(1/a_n)).

theorem PoissonDeclumping.StableToolkit.exists_eventually_le_sub {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {ε : ℝ} (hε : 0 < ε) : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ ∀ᶠ (t : ℕ) in Filter.atTop, ∀ (j : ℕ), ↑j ≤ δ * ↑t → (1 - ε) * a t ≤ a (t - j)

Uniform regular variation below a time: for every ε > 0 there is δ > 0 with a_{t-j} ≥ (1 - ε) a_t for all j ≤ δ t, for all large t.

theorem PoissonDeclumping.StableToolkit.eventually_abs_mul_sub_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {d : ℕ} {L : ℝ} (hloc : LatticeLocal μ a d L) {N m : ℕ → ℕ} (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (hm : (fun (n : ℕ) => ↑(m n)) =o[Filter.atTop] fun (n : ℕ) => ↑(N n)) {z : ℕ → ℝ} (hz : z =o[Filter.atTop] fun (n : ℕ) => a (N n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m n, ∀ (x : ℤ), ↑d ∣ x + ↑(N n - j) → |↑x| ≤ z n → |a (N n) * walkProb μ (↑(N n - j)) x - L| ≤ ε

Microscopic flatness. Let N n → ∞ be a sequence of total lengths, m_n = o(N_n) and z_n = o(a_{N_n}). Then a_{N_n} Ψ_{N_n - j}(x) → L uniformly over j ≤ m_n and lattice-compatible |x| ≤ z_n. (With N n = n: a_n Ψ_{n-j}(x) → L.)

theorem PoissonDeclumping.StableToolkit.eventually_bounds {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {d : ℕ} {L : ℝ} (hloc : LatticeLocal μ a d L) {N m : ℕ → ℕ} (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (hm : (fun (n : ℕ) => ↑(m n)) =o[Filter.atTop] fun (n : ℕ) => ↑(N n)) {z : ℕ → ℝ} (hz : z =o[Filter.atTop] fun (n : ℕ) => a (N n)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m n, ∀ (x : ℤ), ↑d ∣ x + ↑(N n - j) → |↑x| ≤ z n → L / 2 / a (N n) ≤ walkProb μ (↑(N n - j)) x ∧ walkProb μ (↑(N n - j)) x ≤ 2 * L / a (N n)

Two-sided local bounds L / (2 a_{N_n}) ≤ Ψ_{N_n - j}(x) ≤ 2L / a_{N_n}, uniformly over j ≤ m_n (m_n = o(N_n)) and compatible |x| ≤ z_n (z_n = o(a_{N_n})); e.g. Ψ_n(k) ≥ c / a_n for compatible |k| ≤ z_n (line 1647).

theorem PoissonDeclumping.StableToolkit.eventually_abs_div_sub_one_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {d : ℕ} {L : ℝ} (hloc : LatticeLocal μ a d L) {N m : ℕ → ℕ} (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (hm : (fun (n : ℕ) => ↑(m n)) =o[Filter.atTop] fun (n : ℕ) => ↑(N n)) {z : ℕ → ℝ} (hz : z =o[Filter.atTop] fun (n : ℕ) => a (N n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m n, ∀ (x y : ℤ), ↑d ∣ x + ↑(N n - j) → ↑d ∣ y + ↑(N n) → |↑x| ≤ z n → |↑y| ≤ z n → |walkProb μ (↑(N n - j)) x / walkProb μ (↑(N n)) y - 1| ≤ ε

Ratio limit at compatible endpoints. For N_n → ∞, m_n = o(N_n) and z_n = o(a_{N_n}), Ψ_{N_n - j}(x) / Ψ_{N_n}(y) → 1 uniformly over j ≤ m_n and compatible |x|, |y| ≤ z_n (the lattice factor d cancels, lines 877–879).

theorem PoissonDeclumping.StableToolkit.exists_lower_bound_neg_one {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → 0 < walkProb μ (↑n) (-1) → c / a n ≤ walkProb μ (↑n) (-1)

Global lower bound at admissible sizes. One constant c > 0 with Ψ_n(-1) ≥ c / a_n for every n ≥ 1 such that Ψ_n(-1) > 0 (by Dwass, every admissible n): lines 1164, 1231, 1329 ("Ψ_n(-1) ≍ 1/a_n", "P(|𝒯| = n) ≍ 1/(n a_n) along admissible n") and the constant of Corollary cor:pip (line 1653, "for every n ≥ 1").

theorem PoissonDeclumping.StableToolkit.eventually_walkProb_neg_one_pos_iff {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {d : ℕ} {L : ℝ} (hloc : LatticeLocal μ a d L) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < walkProb μ (↑n) (-1) ↔ ↑d ∣ ↑n - 1

Admissible sizes on the lattice. For all large n, Ψ_n(-1) > 0 iff d ∣ n - 1. In the aperiodic case (d = 1) every large n has Ψ_n(-1) > 0, i.e. is admissible (lines 860, 703).

theorem PoissonDeclumping.StableToolkit.eventually_walkLaw_tail_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {M : ℕ → ℕ} {r : ℕ → ℝ} (hM : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ M n) (hr : Filter.Tendsto (fun (n : ℕ) => r n / a (M n)) Filter.atTop Filter.atTop) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ i ≤ M n, (walkLaw μ i).real {x : ℤ | r n < |↑x|} ≤ ε

Uniform tails at small times. If r_n / a_{M_n} → ∞ (e.g. r_n = √(a_{M_n} a_n), RegularlyVaryingSeq.tendsto_sqrt_div), then max_{i ≤ M_n} P(|S_i| > r_n) → 0. This is the form in which the paper uses tightness of (S_{⌊M_n t⌋}/a_{M_n}) (lines 1763–1770) and the convergence in law of S_{M_n}/a_{M_n} (line 1912).