Documentation

BGW.StableTrees.Scalar.LocalLimit

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 α:

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).

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

source
theorem BGW.StableTrees.Scalar.walkProb_coe_nat (μ : PMF ℕ) (n : ℕ) (k : ℤ) :
walkProb μ (↑n) k = (walkLaw μ n).real {k}
source
noncomputable def BGW.StableTrees.Scalar.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.
Instances For
    source
    theorem BGW.StableTrees.Scalar.norm_cexp_neg_mul_I' (t x : ℝ) :
    ‖Complex.exp (-(↑t * ↑x * Complex.I))‖ = 1
    source
    theorem BGW.StableTrees.Scalar.integrable_truncCF {μ : PMF ℕ} {a : ℕ → ℝ} (n : ℕ) :
    MeasureTheory.Integrable (truncCF μ a n) MeasureTheory.volume
    source
    theorem BGW.StableTrees.Scalar.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.

    source
    theorem BGW.StableTrees.Scalar.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)^α).

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

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

    source
    theorem BGW.StableTrees.Scalar.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).

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

    source
    theorem BGW.StableTrees.Scalar.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ℤ.

    source
    theorem BGW.StableTrees.Scalar.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ℤ.