The span of the offspring law and lattice Fourier inversion

Source lines 855–883 ("Periodicity"). The span of μ is d = gcd {i - j : μ_i μ_j > 0} (BGW.StableTrees.Scalar.latticeSpan, defined literally as the greatest common divisor of the differences). For critical μ with μ_1 ≠ 1 we have μ_0 > 0, so every support point is a multiple of d, and X = K - 1 ∈ -1 + dℤ; hence S_n ∈ -n + dℤ (this is the paper's lattice nb + dℤ with the support point b = -1).

• BGW.StableTrees.Scalar.stepCF_add_period: φ(θ + 2π/d) = e^{-2πi/d} φ(θ);
• BGW.StableTrees.Scalar.norm_stepCF_lt_one: |φ(θ)| < 1 for 0 < |θ| ≤ π/d (via Bezout: d is an integer combination of support differences);
• BGW.StableTrees.Scalar.walkLaw_real_singleton_eq_zero: P(S_n = k) = 0 unless d ∣ k + n;
• BGW.StableTrees.Scalar.walkLaw_real_singleton_lattice: for d ∣ k + n, P(S_n = k) = (d/2π) ∫_{-π/d}^{π/d} φ(θ)^n e^{-ikθ} dθ.

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

def BGW.StableTrees.Scalar.supportDiffs (μ : PMF ℕ) : Set ℤ

The differences i - j of points of the support of μ.

Equations

• BGW.StableTrees.Scalar.supportDiffs μ = {m : ℤ | ∃ (i : ℕ) (j : ℕ), μ i ≠ 0 ∧ μ j ≠ 0 ∧ m = ↑i - ↑j}

noncomputable def BGW.StableTrees.Scalar.latticeSpan (μ : PMF ℕ) : ℕ

The span d = gcd {i - j : μ_i μ_j > 0} of the support of μ (source lines 855–858): the greatest natural number dividing every difference of two support points.

Equations

• BGW.StableTrees.Scalar.latticeSpan μ = sSup {D : ℕ | ∀ (i j : ℕ), μ i ≠ 0 → μ j ≠ 0 → ↑D ∣ ↑i - ↑j}

theorem BGW.StableTrees.Scalar.latticeSpan_eq_natAbs_generator (μ : PMF ℕ) : latticeSpan μ = (Submodule.IsPrincipal.generator (Ideal.span (supportDiffs μ))).natAbs

theorem BGW.StableTrees.Scalar.latticeSpan_dvd (μ : PMF ℕ) {i j : ℕ} (hi : μ i ≠ 0) (hj : μ j ≠ 0) : ↑(latticeSpan μ) ∣ ↑i - ↑j

d divides every difference of support points.

theorem BGW.StableTrees.Scalar.latticeSpan_mem_span (μ : PMF ℕ) : ↑(latticeSpan μ) ∈ Ideal.span (supportDiffs μ)

Bezout: d is an integer combination of differences of support points.

theorem BGW.StableTrees.Scalar.latticeSpan_pos {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : 0 < latticeSpan μ

theorem BGW.StableTrees.Scalar.latticeSpan_dvd_of_ne_zero {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {i : ℕ} (hi : μ i ≠ 0) : ↑(latticeSpan μ) ∣ ↑i

Every support point of μ is a multiple of d (since μ_0 > 0).

theorem BGW.StableTrees.Scalar.stepCF_eq_integral {μ : PMF ℕ} (θ : ℝ) : stepCF μ θ = ∫ (k : ℕ), Complex.exp (↑θ * ↑(↑k - 1) * Complex.I) ∂μ.toMeasure

theorem BGW.StableTrees.Scalar.ae_toMeasure_ne_zero {μ : PMF ℕ} : ∀ᵐ (k : ℕ) ∂μ.toMeasure, μ k ≠ 0

theorem BGW.StableTrees.Scalar.stepCF_add_period {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (θ : ℝ) : stepCF μ (θ + 2 * Real.pi / ↑(latticeSpan μ)) = Complex.exp (-(↑(2 * Real.pi / ↑(latticeSpan μ)) * Complex.I)) * stepCF μ θ

Twisted periodicity of φ: φ(θ + 2π/d) = e^{-2πi/d} φ(θ).

theorem BGW.StableTrees.Scalar.eq_one_of_norm_eq_one_of_re_eq_one {w : ℂ} (hn : ‖w‖ = 1) (hr : w.re = 1) : w = 1

theorem BGW.StableTrees.Scalar.exists_int_of_norm_stepCF_eq_one {μ : PMF ℕ} {θ : ℝ} (h : ‖stepCF μ θ‖ = 1) : ∃ (n : ℤ), θ * ↑(latticeSpan μ) = ↑n * (2 * Real.pi)

If |φ(θ)| = 1 then θ d ∈ 2πℤ.

theorem BGW.StableTrees.Scalar.norm_stepCF_lt_one {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {θ : ℝ} (h0 : θ ≠ 0) (hθ : |θ| ≤ Real.pi / ↑(latticeSpan μ)) : ‖stepCF μ θ‖ < 1

Aperiodicity modulo the span: |φ(θ)| < 1 for 0 < |θ| ≤ π/d.

noncomputable def BGW.StableTrees.Scalar.fourierIntegrand (μ : PMF ℕ) (n : ℕ) (k : ℤ) (θ : ℝ) : ℂ

The Fourier integrand F(θ) = φ(θ)^n e^{-ikθ} of P(S_n = k).

Equations

• BGW.StableTrees.Scalar.fourierIntegrand μ n k θ = BGW.StableTrees.Scalar.stepCF μ θ ^ n * Complex.exp (-(↑θ * ↑k * Complex.I))

theorem BGW.StableTrees.Scalar.continuous_fourierIntegrand {μ : PMF ℕ} (n : ℕ) (k : ℤ) : Continuous (fourierIntegrand μ n k)

theorem BGW.StableTrees.Scalar.fourierIntegrand_add_period {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) (k : ℤ) (θ : ℝ) : fourierIntegrand μ n k (θ + 2 * Real.pi / ↑(latticeSpan μ)) = Complex.exp (-(↑(2 * Real.pi / ↑(latticeSpan μ) * (↑n + ↑k)) * Complex.I)) * fourierIntegrand μ n k θ

theorem BGW.StableTrees.Scalar.fourierIntegrand_add_nat_mul_period {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) (k : ℤ) (θ : ℝ) (j : ℕ) : fourierIntegrand μ n k (θ + ↑j * (2 * Real.pi / ↑(latticeSpan μ))) = Complex.exp (-(↑(2 * Real.pi / ↑(latticeSpan μ) * (↑n + ↑k)) * Complex.I)) ^ j * fourierIntegrand μ n k θ

theorem BGW.StableTrees.Scalar.fourierIntegrand_periodic {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) (k : ℤ) : Function.Periodic (fourierIntegrand μ n k) (2 * Real.pi)

theorem BGW.StableTrees.Scalar.intervalIntegrable_fourierIntegrand {μ : PMF ℕ} (n : ℕ) (k : ℤ) (a b : ℝ) : IntervalIntegrable (fourierIntegrand μ n k) MeasureTheory.volume a b

theorem BGW.StableTrees.Scalar.walkLaw_real_singleton_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n : ℕ} {k : ℤ} (h : ¬↑(latticeSpan μ) ∣ k + ↑n) : (walkLaw μ n).real {k} = 0

P(S_n = k) = 0 off the lattice -n + dℤ.

theorem BGW.StableTrees.Scalar.walkLaw_real_singleton_lattice {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) (k : ℤ) (h : ↑(latticeSpan μ) ∣ k + ↑n) : ↑((walkLaw μ n).real {k}) = ↑(latticeSpan μ) / (2 * ↑Real.pi) * ∫ (θ : ℝ) in -(Real.pi / ↑(latticeSpan μ))..Real.pi / ↑(latticeSpan μ), fourierIntegrand μ n k θ

Lattice Fourier inversion: for k ≡ -n (mod d), P(S_n = k) = (d/2π) ∫_{-π/d}^{π/d} φ(θ)^n e^{-ikθ} dθ.