The random-walk toolkit derived from (H_α) (Stage 5)

Source lines 837–883 and the toolbox uses at lines 1029–1041, 1138–1177, 1640–1647, 1987–1994 (inventory B06, B07, B09, B10, B14). The final export is

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

discharging the conditional interface PoissonDeclumping.StableToolkit of PoissonDeclumping.Setup.Toolkit from the hypothesis (H_α) alone. Its fields are proved by:

• regularlyVarying: PoissonDeclumping.Stable.regularlyVaryingSeq (convergence of types);
• sup_le: PoissonDeclumping.Stable.exists_walkProb_le (local limit theorem plus boundedness of d_α, and Ψ_m ≤ 1 ≤ a_N/a_m for the finitely many small m);
• tight: PoissonDeclumping.Stable.tight (weak convergence against the continuous cutoff min(1, (|y| - R)_+), and tightness of each of the finitely many small-time laws);
• lattice: PoissonDeclumping.Stable.latticeLocal, with d = latticeSpan μ and L = d · d_α(0) > 0 (lattice local limit theorem, Lipschitz continuity of d_α, d_α(0) > 0).

The paper's functional convergence in the Skorokhod J_1 topology (B07) is not proved: the toolkit only needs marginal tightness (see PoissonDeclumping.StableToolkit.tight), and the Skorokhod-representation step of B14 is replaced by the deterministic equicontinuity field.

theorem PoissonDeclumping.Stable.exists_walkProb_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (C : ℝ), ∀ (m : ℕ), 1 ≤ m → ∀ (x : ℤ), walkProb μ (↑m) x ≤ C / a m

Uniform local bound (inventory B10, "the local bound following from eq:LL", source lines 1140, 1161): Ψ_m(x) ≤ C / a_m for all m ≥ 1 and all x ∈ ℤ.

noncomputable def PoissonDeclumping.Stable.cutoffFn (R : ℝ) : BoundedContinuousFunction ℝ ℝ

The bounded continuous cutoff y ↦ min 1 (max 0 (|y| - R)).

Equations

• PoissonDeclumping.Stable.cutoffFn R = BoundedContinuousFunction.ofNormedAddCommGroup (fun (y : ℝ) => min 1 (max 0 (|y| - R))) ⋯ 1 ⋯

theorem PoissonDeclumping.Stable.cutoffFn_apply (R y : ℝ) : (cutoffFn R) y = min 1 (max 0 (|y| - R))

theorem PoissonDeclumping.Stable.tight {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ), ∀ (m : ℕ), 1 ≤ m → (walkLaw μ m).real {x : ℤ | K * a m < |↑x|} ≤ ε

Tightness of S_m / a_m (inventory B07 in marginal form): sup_{m ≥ 1} P(|S_m| > K a_m) → 0 as K → ∞.

theorem PoissonDeclumping.Stable.latticeLocal {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : LatticeLocal μ a (latticeSpan μ) (↑(latticeSpan μ) * stableDensity α 0)

The lattice local limit theorem in the toolkit form (LatticeLocal), with d = latticeSpan μ and L = d · d_α(0) > 0.

theorem PoissonDeclumping.Stable.stableToolkit {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : StableToolkit μ α a

The stable random-walk toolkit, derived from (H_α). Every field of PoissonDeclumping.StableToolkit follows from StableDomain μ α a alone.