Canonical norming #

Ported from BGWLeaves/StableAnalysis/Norming.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

Canonical norming and Theorem 1.10(i)--(ii) #

The domain criterion selects the tail, infinite-variance Gaussian, or finite-variance Gaussian branch. Canonical attraction and convergence of types identify the norming. Monotonicity and sequence regular variation give the slowly varying real floor extension. The earlier finite-variance helpers are retained below.

source

theorem BGW.StableTrees.Attraction.Norming.locallimit_i (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hDA : ∃ (b : ℕ → ℝ), IsStableAttracted ν θ (mean ν) b) :

IsStableAttracted ν θ (mean ν) (norming ν θ)

Theorem 1.10(i), with the corrected canonical norming.

source

theorem BGW.StableTrees.Attraction.Norming.norming_isEquivalent (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {b : ℕ → ℝ} (hb : IsStableAttracted ν θ (mean ν) b) :

Filter.Tendsto (fun (n : ℕ) => norming ν θ n / b n) Filter.atTop (nhds 1)

The corrected canonical norming is equivalent to every attracting norming.

source

theorem BGW.StableTrees.Attraction.Norming.locallimit_ii (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hDA : ∃ (b : ℕ → ℝ), IsStableAttracted ν θ (mean ν) b) :

Monotone (norming ν θ) ∧ SlowlyVarying fun (x : ℝ) => norming ν θ ⌊x⌋₊ / x ^ (1 / θ)

Theorem 1.10(ii): monotonicity and a slowly varying real floor extension.