Uniform characteristic-function bounds (Stage 3)

Source lines 862–883 (the analytic input of the local limit theorem, Ibragimov–Linnik Theorem 4.2.1). With φ = stepCF μ:

• BGW.StableTrees.Scalar.exists_norm_stepCF_pow_le_exp: there are γ, c, δ > 0, A and N with |φ(t/a_n)|^n ≤ exp(-c|t|^γ) for n ≥ N, A ≤ |t| ≤ δ a_n;
• BGW.StableTrees.Scalar.exists_norm_stepCF_le_of_le_abs: sup_{δ ≤ |θ| ≤ π/d} |φ(θ)| < 1.

Departure from the classical route. The classical proof bounds 1 - |φ(θ)| below by the truncated second moment θ² ∑_{j ≤ 1/|θ|} j² μ_j and uses its regular variation. Here we use instead only the already-proved convergence |φ(s/a_m)|^m → exp(cos(πα/2)|s|^α) uniformly for s ∈ [1,2] (a compactness argument), a_{m+1}/a_m → 1 and the Potter bound for the monotone regularly varying sequence a: for θ small, the first m with θ a_m ≥ 1 satisfies |φ(θ)|^m ≤ q < 1, and n/m ≥ (|t|/2C)^{1/β}. The truncated-second-moment clause of (H_α) (whose slowly varying witness need not be measurable) is not used.

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

theorem BGW.StableTrees.Scalar.stepCF_neg (μ : PMF ℕ) (θ : ℝ) : stepCF μ (-θ) = (starRingEnd ℂ) (stepCF μ θ)

theorem BGW.StableTrees.Scalar.norm_stepCF_neg (μ : PMF ℕ) (θ : ℝ) : ‖stepCF μ (-θ)‖ = ‖stepCF μ θ‖

theorem BGW.StableTrees.Scalar.exists_norm_stepCF_pow_le_of_mem_Icc {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) (K : ℝ) : ∃ q < 1, ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ s ∈ Set.Icc 1 K, ‖stepCF μ (s / a m)‖ ^ m ≤ q

Uniformly on a compact range s ∈ [1, K] of the rescaled argument, |φ(s/a_m)|^m stays below a constant q < 1 for all large m.

theorem BGW.StableTrees.Scalar.exists_norm_stepCF_pow_le_exp {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : ∃ (γ : ℝ) (c : ℝ) (A : ℝ) (δ : ℝ), 0 < γ ∧ 0 < c ∧ 0 < δ ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (t : ℝ), A ≤ |t| → |t| ≤ δ * a n → ‖stepCF μ (t / a n)‖ ^ n ≤ Real.exp (-c * |t| ^ γ)

Characteristic-function bound (Stage 3). There are γ, c > 0, A, δ > 0 and N such that for n ≥ N and A ≤ |t| ≤ δ a_n, |φ(t/a_n)|^n ≤ exp(-c |t|^γ). The proof uses only the convergence |φ(s/a_m)|^m → exp(cos(πα/2)|s|^α) uniformly for s ∈ [1,2], the ratio a_{m+1}/a_m → 1, and the Potter bound a_n ≤ C (n/m)^β a_m (β = 1/α + 1).

theorem BGW.StableTrees.Scalar.exists_norm_stepCF_le_of_le_abs {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {δ : ℝ} (hδ : 0 < δ) : ∃ (q : ℝ), 0 ≤ q ∧ q < 1 ∧ ∀ (θ : ℝ), δ ≤ |θ| → |θ| ≤ Real.pi / ↑(latticeSpan μ) → ‖stepCF μ θ‖ ≤ q

Away from the dual lattice: sup_{δ ≤ |θ| ≤ π/d} |φ(θ)| < 1.