Scalar stable analysis (M3): definitions and proved bridges #
Source: arXiv:1110.2163v4, largetrees_final.tex, Section 1 (Proposition 1.7, Definitions 1.8,
Theorem 1.10, Lemma 1.11, Remarks 1.9 and 1.12) and Sections 3 and 6 (Lemma 3.4, Theorem 3.5,
the Gaussian convolution of Section 6).
This file contains every definition of milestone M3 and every proved lemma that does not depend on
the statements still to be proved (those are in BGW.StableTrees.Attraction, and the proved results
that use them are in BGW.StableTrees.Attraction.Consequences). It contains no proof holes.
The paper's norming constant Γ(1-θ)^{1/θ} and the norming √(n K(z_n)) are not correct as
printed; norming is the corrected one (printedConstant_neg, printedNorming_gauss).
Ported from BGWLeaves/StableAnalysis/Defs.lean of the author's arXiv:1110.2163v4
formalization (local snapshot of 6 November 2026).
0. Walks with an arbitrary integer step law #
n-fold convolution power of a step law on ℤ; the empty sum is δ₀.
For ν = stepLaw μ this is walkLaw μ (intWalk_stepLaw).
Equations
Instances For
P[W_n = k] for the walk with step law ν.
Equations
Instances For
Mean and variance of a law on ℤ.
Instances For
The second central moment of a law on ℤ.
Equations
- BGW.StableTrees.Attraction.variance ν = ∫ (z : ℤ), (↑z - BGW.StableTrees.Attraction.mean ν) ^ 2 ∂ν
Instances For
Definition 1.8: the law is lattice if its support lies in b + dℤ for some d ≥ 2.
On the countable space ℤ, "support contained in" is "almost surely in".
Equations
Instances For
d is the span: the largest d with support in some b + dℤ, in the divisibility sense
(every admissible d' divides d); 0 < d excludes point masses.
Equations
Instances For
2. Lattice and non-lattice laws (1.8, 1.9 rem:non-lattice) #
Aperiodic μ is latticeSpan μ = 1 for a critical nondegenerate law.
Remark 1.9: for critical, aperiodic μ (with μ 1 ≠ 1) the law ν of K - 1 is
non-lattice. Uses μ 0 > 0.
3. The printed norming (1.10): the constant and the positive replacement #
Γ(1-θ) < 0 for 1 < θ < 2: the base of the printed constant Γ(1-θ)^{1/θ} is
negative.
The printed real power Γ(1-θ)^{1/θ}, read with Lean's rpow on a negative base, is
negative (exp(..)·cos(π/θ) < 0), so the printed formula is not a norming as written. Reading it as
|Γ(1-θ)|^{1/θ} gives a positive constant, which is the correct one: the norming is
(-Γ(1-θ))^{1/θ} times the tail quantile (negGamma_eq).
The positive constant: for Laplace exponent u ^ θ (E exp(-u X) = exp(u^θ)) and
n P[W > a_n x] → (C x)^{-θ}, the norming constant is C^θ = θ Γ(-θ) = -Γ(1-θ) = Γ(2-θ)/(θ-1) > 0.
sup {z ≥ 0 : K(z)/z² ≥ 1/n} (sSup ∅ = 0 as in the printed convention;
at z = 0 Lean's K 0 / 0 = 0 < 1/n, so 0 is not in the set for n ≥ 1).
Equations
Instances For
The corrected norming a_n of Theorem 1.10, for Laplace exponent u ^ θ:
σ √(n/2) if the variance is finite; (-Γ(1-θ))^{1/θ} · inf{x : P[W₁>x] ≤ 1/n} if the variance
is infinite and θ < 2; √(n K(z_n) / 2) (note the factor 1/2) if the variance is
infinite and θ = 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The norming as printed (Theorem 1.10): constant Γ(1-θ)^{1/θ} (negative base) and
√(n K(z_n)) (no 1/2). Kept only to document the discrepancies.
Equations
- One or more equations did not get rendered due to their size.
Instances For
In the case σ² = ∞, θ = 2 the printed norming is √2 times the corrected one.
(With K ≡ σ² the printed formula would give σ√n, not σ√(n/2).)
Weak convergence of (W_n - n m) / a_n to the law X_1 with Laplace transform
exp(λ^θ); a_n > 0 eventually (the explicit quantile norming vanishes at small n).
This is the definition of the domain of
attraction with centering n m, normalized to the spectrally positive law of 1.10.
For ν = stepLaw μ and m = 0 it is StableDomain μ θ a without monotonicity.
- converges : ∃ (X : MeasureTheory.Measure ℝ), MeasureTheory.IsProbabilityMeasure X ∧ (∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂X = Real.exp (lam ^ θ)) ∧ ∀ (f : BoundedContinuousFunction ℝ ℝ), Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), f x ∂MeasureTheory.Measure.map (fun (z : ℤ) => (↑z - ↑n * m) / a n) (intWalk ν n)) Filter.atTop (nhds (∫ (x : ℝ), f x ∂X))
Instances For
Bridge to BGW's StableDomain: replace the first N terms by a N (this keeps
monotonicity and gives positivity for all n ≥ 1); the new sequence agrees with a eventually.
Proved bridge. For a critical aperiodic μ with StableDomain, the existing
Scalar.localLimit_aperiodic is llt_abstract for ν = stepLaw μ, m = 0.
5. Lemma 1.11 (lem:locallimit) and Remark 1.12 (rem:lattice) #
ζ(τ) ≥ n, including infinite trees (they have probability zero in the critical case).
Equations
Instances For
Kemperman at ℓ = 1: n P[ζ = n] = P[W_n = -1] for n ≥ 1.
The size law with its exact constant, on the admissible lattice
d ∣ n - 1 (d = latticeSpan μ): n a_n P[ζ = n] - d p₁(0) → 0.
This covers the periodic case (rem:lattice) and, for d = 1, lem:locallimit.
Lemma 1.11, first half, in terms of any StableDomain norming a (a_n = B_n = n^{1/θ} h(n)): P[ζ = n] ∼ p₁(0) / (n a_n), for aperiodic μ.
Remark 1.12 (both halves, in terms of d = latticeSpan μ, the span of supp μ
since μ 0 > 0): for large n, P[ζ = n] > 0 iff d ∣ n - 1.
The aperiodic corollary of 1.12: every large n is admissible.
6. Finite variance: reuse of stableDomain_of_finiteVariance, and the ratio check #
Proved reuse. For a critical nondegenerate law with finite variance, the corrected
norming at index 2 is exactly the sequence of Scalar.stableDomain_of_finiteVariance.
The law of Y = K - 1 given K ≥ 1 (eq:Y), on ℤ: P[Y = i] = μ(i+1)/(1-μ₀).
Equations
- BGW.StableTrees.Attraction.etaLaw μ = MeasureTheory.Measure.map (fun (k : ℕ) => ↑k - 1) μ.toMeasure[|Set.Ici 1]
Instances For
Proved algebra: that limit squared, μ₀ σ'^2/σ², is strictly smaller than
c = μ₀/(1-μ₀) for 0 < μ₀ < 1; so B'_n / B_{n/μ₀} → c^{1/θ} is false in finite variance.
8. The Gaussian density #
9. Additions after audit #
F₀(u) = (2π(1-μ₀))^{-1/2} exp(-μ₀² u²/(2(1-μ₀))) (line 1849: F₀(u) = √μ₀ F(μ₀^{3/2}u));
μ₀ F₀ is the N(0,(1-μ₀)/μ₀²) density.
Equations
Instances For
G₀(u,x) of line 1850 in the finite-variance case θ = 2, with c = μ₀/(1-μ₀),
c^{1/2} written √c, c^{3/2} = c √c, σ' = sp.
Equations
Instances For
Corrected Gaussian identity (finite variance, line 1937-1940). With
r = √μ₀ σ'/σ (σ'^2 = σ²/(1-μ₀) - μ₀/(1-μ₀)²), the convolution μ₀ ∫ F₀(u) G₀(u,x) du
equals r p₁(r x). The paper's c^{1/2} p₁(c^{1/2} x) is wrong: r < c^{1/2}
(r_lt_sqrt_c); at x = j/B'_n, r x = j / B_{n/μ₀} as printed, only the prefactor and the
inner scaling by r (not √c) are corrected.
The printed hypothesis (H_θ)(ii) made precise: finite variance and θ = 2
(BGW proves finite variance forces θ = 2, Scalar.alpha_eq_two_of_finiteVariance), or
μ[j,∞) = j^{-θ} L(j) with L slowly varying (measurable, nonnegative).
Equations
- One or more equations did not get rendered due to their size.