Canonical attraction

The Gaussian Abelian argument reuses the square-weighted absolute-step measure and the Taylor/Fubini identities from LaplaceExpansion. At Karamata index zero, its transform is asymptotic to the truncated second moment. Two integrations supply the factor 1/2; unboundedness makes the atom and centering corrections negligible. The one-step expansions then imply attraction through Laplace continuity. For finite positive variance, a general characteristic-function CLT supplies the Gaussian limit directly, without a lower support assumption. Ported from BGWLeaves/StableAnalysis/CanonicalAttraction.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_dampedSecondMoment_ratio {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (x : ℝ) => KaramataTransforms.laplace (LaplaceExpansion.secondMomentMeasure ν) (1 / x) / truncSecondMoment ν x) Filter.atTop (nhds 1)

At the Gaussian boundary the damped second moment is asymptotic to K.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_absolute_remainder_ratio {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (x : ℝ) => (∫ (z : ℤ), Real.exp (-(1 / x) * |↑z|) - 1 + 1 / x * |↑z| ∂ν) / (truncSecondMoment ν x / x ^ 2)) Filter.atTop (nhds (1 / 2))

The absolute-step exponential remainder on the Gaussian scale.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_exp_remainder_ratio_zero {ν : MeasureTheory.Measure ℤ} (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) (m : ℝ) : Filter.Tendsto (fun (x : ℝ) => (Real.exp (m / x) - 1 - m / x) / (truncSecondMoment ν x / x ^ 2)) Filter.atTop (nhds 0)

Every fixed deterministic quadratic error is negligible when K → ∞.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_uncentered_remainder_ratio {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (x : ℝ) => (∫ (z : ℤ), Real.exp (-(1 / x) * ↑z) ∂ν - 1 + mean ν / x) / (truncSecondMoment ν x / x ^ 2)) Filter.atTop (nhds (1 / 2))

The uncentered Gaussian Laplace remainder.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_centeredLaplace_ratio {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (x : ℝ) => (LaplaceExpansion.centeredLaplace ν (1 / x) - 1) / (truncSecondMoment ν x / x ^ 2)) Filter.atTop (nhds (1 / 2))

Gaussian D1: the centered remainder is asymptotic to K(x)/(2 x²).

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_centeredLaplace_isEquivalent {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Asymptotics.IsEquivalent (nhdsWithin 0 (Set.Ioi 0)) (fun (s : ℝ) => LaplaceExpansion.centeredLaplace ν s - 1) fun (s : ℝ) => s ^ 2 * truncSecondMoment ν (1 / s) / 2

Gaussian D1 in asymptotic-equivalence form at zero from the right.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_norming_tendsto_atTop {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Filter.Tendsto (norming ν 2) Filter.atTop Filter.atTop

The Gaussian canonical norming diverges.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_norming_moment_limit {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (n : ℕ) => ↑n * truncSecondMoment ν (norming ν 2 n / lam) / (norming ν 2 n / lam) ^ 2) Filter.atTop (nhds (2 * lam ^ 2))

Slow variation and the exact Gaussian crossing identify the scaled moment.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.gaussian_norming_centeredLaplace_limit {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (n : ℕ) => ↑n * (LaplaceExpansion.centeredLaplace ν (lam / norming ν 2 n) - 1)) Filter.atTop (nhds (lam ^ 2))

Gaussian D1: the one-step limit on the canonical norming.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.isStableAttracted_of_centered_one_step_limit {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {b : ℕ → ℝ} (hb : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < b n) (hL : ∀ (lam : ℝ), 0 < lam → Filter.Tendsto (fun (n : ℕ) => ↑n * (LaplaceExpansion.centeredLaplace ν (lam / b n) - 1)) Filter.atTop (nhds (lam ^ θ))) : IsStableAttracted ν θ (mean ν) b

A one-step centered Laplace expansion gives attraction after taking powers. The centering factor here is exactly the one used by the continuity provider.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.isStableAttracted_of_regVary_tail {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {θ : ℝ} (hθ1 : 1 < θ) (hθ2 : θ < 2) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)) : IsStableAttracted ν θ (mean ν) (norming ν θ)

D2(i): regularly varying right tail, with index strictly between one and two.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.isStableAttracted_of_slowlyVarying_moment {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : IsStableAttracted ν 2 (mean ν) (norming ν 2)

D2(ii): the infinite-variance Gaussian criterion.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.isStableAttracted_finiteVariance_stepLaw {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfin : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) : IsStableAttracted (stepLaw μ) 2 (mean (stepLaw μ)) (norming (stepLaw μ) 2)

D2(iii) in the critical offspring-law setting already covered by BGW.

theorem BGW.StableTrees.Attraction.CanonicalAttraction.isStableAttracted_of_finiteVariance {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hsq : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) (hvar : 0 < variance ν) : IsStableAttracted ν 2 (mean ν) (norming ν 2)

D2(iii) for a general integer law of finite, strictly positive variance. No lower support bound is needed for this CLT proof. Positive variance excludes the degenerate case, whose canonical norming is identically zero.