Finite-variance normalization

The finite-variance assertion at source line 864: the normalizing sequence in StableDomain is asymptotic to a positive constant times √n.

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

theorem BGW.StableTrees.Scalar.offspring_integral_eq_one {μ : PMF ℕ} (hc : IsCritical μ) : ∫ (j : ℕ), ↑j ∂μ.toMeasure = 1

theorem BGW.StableTrees.Scalar.memLp_step_of_memLp_offspring {μ : PMF ℕ} (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : MeasureTheory.MemLp (fun (z : ℤ) => ↑z) 2 (stepLaw μ)

theorem BGW.StableTrees.Scalar.step_integral_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : ∫ (z : ℤ), ↑z ∂stepLaw μ = 0

theorem BGW.StableTrees.Scalar.step_secondMoment_pos {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : 0 < ∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ

theorem BGW.StableTrees.Scalar.tendsto_charFun_moving {P : ℕ → MeasureTheory.ProbabilityMeasure ℝ} {Q : MeasureTheory.ProbabilityMeasure ℝ} (hP : Filter.Tendsto P Filter.atTop (nhds Q)) {s : ℕ → ℝ} {t : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds t)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.charFun (↑(P n)) (s n)) Filter.atTop (nhds (MeasureTheory.charFun (↑Q) t))

Weak convergence of probability measures also controls characteristic functions at moving arguments. This is the equicontinuity argument used for the stable normalization.

noncomputable def BGW.StableTrees.Scalar.finiteVarianceLaw (μ : PMF ℕ) (σ : ℝ) (n : ℕ) : MeasureTheory.ProbabilityMeasure ℝ

The law of the n-step offspring-minus-one walk divided by σ * Real.sqrt n.

Equations

• BGW.StableTrees.Scalar.finiteVarianceLaw μ σ n = ⟨BGW.StableTrees.Scalar.scaledLaw μ (fun (n : ℕ) => σ * √↑n) n, ⋯⟩

noncomputable def BGW.StableTrees.Scalar.standardGaussian : MeasureTheory.ProbabilityMeasure ℝ

The centered real Gaussian probability measure with variance one.

Equations

• BGW.StableTrees.Scalar.standardGaussian = ⟨ProbabilityTheory.gaussianReal 0 1, BGW.StableTrees.Scalar.standardGaussian._proof_1⟩

theorem BGW.StableTrees.Scalar.norm_charFun_finiteVarianceLaw (μ : PMF ℕ) (σ : ℝ) (n : ℕ) (t : ℝ) : ‖MeasureTheory.charFun (↑(finiteVarianceLaw μ σ n)) t‖ = ‖stepCF μ (t / (σ * √↑n))‖ ^ n

theorem BGW.StableTrees.Scalar.finiteVariance_clt {μ : PMF ℕ} (hc : IsCritical μ) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) {σ : ℝ} (hσ : 0 < σ) (hσsq : σ ^ 2 = ∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ) : Filter.Tendsto (finiteVarianceLaw μ σ) Filter.atTop (nhds standardGaussian)

The ordinary central limit theorem for the walk, using its genuine finite variance.

theorem BGW.StableTrees.Scalar.finiteVariance_norming_ratio {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) {σ : ℝ} (hσ : 0 < σ) (hσsq : σ ^ 2 = ∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ) : Filter.Tendsto (fun (n : ℕ) => a n / (σ * √↑n)) Filter.atTop (nhds ((-1 / 2 / Real.cos (Real.pi * α / 2)) ^ (1 / α)))

Comparison with the ordinary central limit scaling fixes the stable normalization up to an explicit positive constant.

theorem BGW.StableTrees.Scalar.exists_norming_isEquivalent_sqrt {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : ∃ (c : ℝ), 0 < c ∧ Asymptotics.IsEquivalent Filter.atTop a fun (n : ℕ) => c * √↑n

Finite-variance normalization (source line 864, inventory B09): under the paper's standing hypothesis, any finite-variance offspring law has a_n ∼ c √n for some c > 0.

theorem BGW.StableTrees.Scalar.alpha_eq_two_of_finiteVariance {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : α = 2

A nondegenerate finite-variance offspring law can only have stable index 2.

theorem BGW.StableTrees.Scalar.summable_offspring_secondMoment {μ : PMF ℕ} (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : Summable fun (j : ℕ) => ↑j ^ 2 * (μ j).toReal

theorem BGW.StableTrees.Scalar.finiteVariance_second_moment {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : ∃ (ℓ : ℝ → ℝ), SlowlyVarying ℓ ∧ ∀ (n : ℕ), 1 ≤ n → ∑ j ∈ Finset.range (n + 1), ↑j ^ 2 * (μ j).toReal = ℓ ↑n * ↑n ^ (2 - 2)

theorem BGW.StableTrees.Scalar.stableDomain_of_finiteVariance {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : StableDomain μ 2 fun (n : ℕ) => √(∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ) / √2 * √↑n

Every nondegenerate critical finite-variance offspring law satisfies the paper's complete stable-domain hypothesis with index 2 and normalization σ √n / √2. The variance and the truncated-moment slowly varying function are constructed from the actual offspring law.

theorem BGW.StableTrees.Scalar.inStableDomain_of_finiteVariance {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : InStableDomain μ

The finite-variance special case of the stable-domain characterization.