The (lattice) local limit theorem (Stage 4)

Source lines 855–883 (inventory B09, eq:LL and its lattice version; the paper cites Ibragimov–Linnik, Theorem 4.2.1). Under (H_α) alone, with d = latticeSpan μ the span of μ (periodic laws allowed) and d_α = stableDensity α:

• PoissonDeclumping.Stable.localLimit: uniformly over k ∈ -n + dℤ, |a_n P(S_n = k) - d · d_α(k / a_n)| → 0;
• PoissonDeclumping.Stable.walkProb_eq_zero_of_not_dvd: P(S_n = k) = 0 off -n + dℤ;
• PoissonDeclumping.Stable.localLimit_aperiodic: the aperiodic statement eq:LL;
• PoissonDeclumping.Stable.localLimit_of_support: the paper's form with the lattice nb + dℤ for an arbitrary support point b of X_1.

Proof: Fourier inversion on ℤ reduced to [-π/d, π/d] by the twisted periodicity of φ, rescaling θ = t/a_n, and the L¹ convergence ∫ |1_{|t| ≤ π a_n/d} φ(t/a_n)^n - exp((-it)^α)| dt → 0 (dominated convergence on |t| ≤ δ a_n with the Stage 3 bound, and a_n q^n → 0 on δ a_n ≤ |t| ≤ π a_n/d).

theorem PoissonDeclumping.Stable.walkProb_coe_nat (μ : PMF ℕ) (n : ℕ) (k : ℤ) : walkProb μ (↑n) k = (walkLaw μ n).real {k}

noncomputable def PoissonDeclumping.Stable.truncCF (μ : PMF ℕ) (a : ℕ → ℝ) (n : ℕ) (t : ℝ) : ℂ

The rescaled truncated characteristic function t ↦ 1_{|t| ≤ π a_n/d} φ(t/a_n)^n.

Equations

• One or more equations did not get rendered due to their size.

theorem PoissonDeclumping.Stable.norm_cexp_neg_mul_I' (t x : ℝ) : ‖Complex.exp (-(↑t * ↑x * Complex.I))‖ = 1

theorem PoissonDeclumping.Stable.integrable_truncCF {μ : PMF ℕ} {a : ℕ → ℝ} (n : ℕ) : MeasureTheory.Integrable (truncCF μ a n) MeasureTheory.volume

theorem PoissonDeclumping.Stable.mul_walkLaw_real_eq {μ : PMF ℕ} {a : ℕ → ℝ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n : ℕ} (han : 0 < a n) {k : ℤ} (hk : ↑(latticeSpan μ) ∣ k + ↑n) : ↑(a n * (walkLaw μ n).real {k}) = ↑(latticeSpan μ) / (2 * ↑Real.pi) * ∫ (t : ℝ), truncCF μ a n t * Complex.exp (-(↑t * ↑(↑k / a n) * Complex.I))

The rescaled lattice Fourier formula: for d ∣ k + n and a_n > 0, a_n P(S_n = k) = (d/2π) ∫ 1_{|t| ≤ π a_n/d} φ(t/a_n)^n e^{-itk/a_n} dt.

theorem PoissonDeclumping.Stable.abs_mul_walkLaw_real_sub_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {n : ℕ} (han : 0 < a n) {k : ℤ} (hk : ↑(latticeSpan μ) ∣ k + ↑n) : |a n * (walkLaw μ n).real {k} - ↑(latticeSpan μ) * stableDensity α (↑k / a n)| ≤ ↑(latticeSpan μ) / (2 * Real.pi) * ∫ (t : ℝ), ‖truncCF μ a n t - stableCF α t‖

The local limit error is controlled, uniformly in k, by the L¹ distance between the truncated rescaled characteristic function and exp((-it)^α).

theorem PoissonDeclumping.Stable.tendsto_integral_norm_truncCF_sub {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ), ‖truncCF μ a n t - stableCF α t‖) Filter.atTop (nhds 0)

The L¹ convergence behind the local limit theorem: ∫ |1_{|t| ≤ π a_n/d} φ(t/a_n)^n - exp((-it)^α)| dt → 0.

theorem PoissonDeclumping.Stable.localLimit {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {ε : ℝ} (hε : 0 < ε) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (k : ℤ), ↑(latticeSpan μ) ∣ k + ↑n → |a n * walkProb μ (↑n) k - ↑(latticeSpan μ) * stableDensity α (↑k / a n)| ≤ ε

Lattice local limit theorem (source lines 860–876: eq:LL and its lattice version). With d = latticeSpan μ the span of μ, uniformly over the lattice -n + dℤ, a_n P(S_n = k) - d · d_α(k / a_n) → 0.

theorem PoissonDeclumping.Stable.walkProb_eq_zero_of_not_dvd {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {n : ℕ} {k : ℤ} (hk : ¬↑(latticeSpan μ) ∣ k + ↑n) : walkProb μ (↑n) k = 0

Off the lattice -n + dℤ the walk has probability zero (source lines 876–877).

theorem PoissonDeclumping.Stable.localLimit_aperiodic {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) (h1 : latticeSpan μ = 1) {ε : ℝ} (hε : 0 < ε) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (k : ℤ), |a n * walkProb μ (↑n) k - stableDensity α (↑k / a n)| ≤ ε

Aperiodic local limit theorem (eq:LL, source line 862): if d = 1, then sup_{k ∈ ℤ} |a_n P(S_n = k) - d_α(k/a_n)| → 0.

theorem PoissonDeclumping.Stable.dvd_sub_mul_iff {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {j : ℕ} (hj : μ j ≠ 0) (n : ℕ) (k : ℤ) : ↑(latticeSpan μ) ∣ k - ↑n * (↑j - 1) ↔ ↑(latticeSpan μ) ∣ k + ↑n

The paper's description of the lattice: for any support point b of X_1 (i.e. μ_{b+1} > 0), k ∈ nb + dℤ iff k ∈ -n + dℤ.

theorem PoissonDeclumping.Stable.localLimit_of_support {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {j : ℕ} (hj : μ j ≠ 0) : (∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (k : ℤ), ↑(latticeSpan μ) ∣ k - ↑n * (↑j - 1) → |a n * walkProb μ (↑n) k - ↑(latticeSpan μ) * stableDensity α (↑k / a n)| ≤ ε) ∧ ∀ (n : ℕ) (k : ℤ), ¬↑(latticeSpan μ) ∣ k - ↑n * (↑j - 1) → walkProb μ (↑n) k = 0

Lattice local limit theorem in the paper's form (source lines 868–876): for every support point b = j - 1 of X_1, uniformly over k ∈ nb + dℤ, |a_n P(S_n = k) - d · d_α(k/a_n)| → 0, and P(S_n = k) = 0 for k ∉ nb + dℤ.