Local bounds and scalar tightness

Both estimates are derived from StableDomain alone. All positive-time bounds retain 1 ≤ m; no condition is imposed on the normalizer at time zero.

Adapted from PoissonDeclumping/Stable/ToolkitProof.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0).

theorem BGW.StableTrees.Scalar.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 BGW.StableTrees.Scalar.cutoffFn (R : ℝ) : BoundedContinuousFunction ℝ ℝ

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

Equations

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

theorem BGW.StableTrees.Scalar.cutoffFn_apply (R y : ℝ) : (cutoffFn R) y = min 1 (max 0 (|y| - R))

theorem BGW.StableTrees.Scalar.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 → ∞.