Gaussian branch (index θ = 2) of stable analysis

The truncated second moment and Gaussian crossing sequence results cover the index-two branch. Ported from BGWLeaves/StableAnalysis/GaussianBranch.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

1. Abstract tail with index -2

2. Truncated second moments

theorem BGW.StableTrees.Attraction.GaussianBranch.truncSecondMoment_nonneg' {ν : MeasureTheory.Measure ℤ} (x : ℝ) : 0 ≤ truncSecondMoment ν x

theorem BGW.StableTrees.Attraction.GaussianBranch.truncSecondMoment_mono {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] : Monotone (truncSecondMoment ν)

K = truncSecondMoment ν is nondecreasing on all of ℝ.

theorem BGW.StableTrees.Attraction.GaussianBranch.truncSecondMoment_floor {ν : MeasureTheory.Measure ℤ} (x : ℝ) : truncSecondMoment ν x = truncSecondMoment ν ↑⌊x⌋

K(x) = K(⌊x⌋): the truncation level only matters through its integer part.

theorem BGW.StableTrees.Attraction.GaussianBranch.truncSecondMoment_tendsto_atTop {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop

Infinite second moment forces K → ∞.

3. (B3-a) Tail regularly varying of index -2

theorem BGW.StableTrees.Attraction.GaussianBranch.truncSecondMoment_slowlyVarying_of_regVary (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hneg : ν {z : ℤ | z < -1} = 0) (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) (hT : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-2)) : SlowlyVarying (truncSecondMoment ν) ∧ Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop

(B3-a) Let ν be a probability law on ℤ with ν {z < -1} = 0 and infinite second moment. If the right tail T(x) = ν {z > x} is regularly varying of index -2, then the truncated second moment K = truncSecondMoment ν is slowly varying (ratio form K(c x)/K(x) → 1) and unbounded. (The proof does not use T beyond monotonicity and regular variation at the dyadic points: 2 ∫₀ˣ u T = K + x² T - ν{-1} and x² T(x) = o(∫₀ˣ u T).)

4. (C3) The Gaussian crossing sequence

theorem BGW.StableTrees.Attraction.GaussianBranch.not_integrable_of_tendsto_atTop {ν : MeasureTheory.Measure ℤ} (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν

K is not bounded below an infinite second moment: if K → ∞ the second moment is infinite.

theorem BGW.StableTrees.Attraction.GaussianBranch.gaussQuantile_sq_eventually {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < gaussQuantile ν n ∧ gaussQuantile ν n ^ 2 = ↑n * truncSecondMoment ν (gaussQuantile ν n)

(C3-a) If K = truncSecondMoment ν is slowly varying and unbounded, then eventually g_n = gaussQuantile ν n is positive and the crossing is an equality: g_n² = n K(g_n) (K is right continuous, being constant on [k, k+1)).

theorem BGW.StableTrees.Attraction.GaussianBranch.gaussQuantile_tendsto_atTop {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => gaussQuantile ν n) Filter.atTop Filter.atTop

(C3-b) g_n → ∞, and hence K(g_n) → ∞.

theorem BGW.StableTrees.Attraction.GaussianBranch.truncSecondMoment_gaussQuantile_tendsto_atTop {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => truncSecondMoment ν (gaussQuantile ν n)) Filter.atTop Filter.atTop

theorem BGW.StableTrees.Attraction.GaussianBranch.gaussQuantile_floor_div {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) {l : ℝ} (hl : 0 < l) : Filter.Tendsto (fun (n : ℕ) => gaussQuantile ν ⌊l * ↑n⌋₊ / gaussQuantile ν n) Filter.atTop (nhds (l ^ (1 / 2)))

(C3-c) The Gaussian crossing sequence is regularly varying of index 1/2: g_{⌊l n⌋} / g_n → l^{1/2}.

theorem BGW.StableTrees.Attraction.GaussianBranch.norming_two_eventually_eq {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : ∀ᶠ (n : ℕ) in Filter.atTop, norming ν 2 n = gaussQuantile ν n / √2

(C3-d) Eventually a_n = norming ν 2 n = g_n / √2 (since g_n² = n K(g_n)).

theorem BGW.StableTrees.Attraction.GaussianBranch.norming_two_floor_div {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) {l : ℝ} (hl : 0 < l) : Filter.Tendsto (fun (n : ℕ) => norming ν 2 ⌊l * ↑n⌋₊ / norming ν 2 n) Filter.atTop (nhds (l ^ (1 / 2)))

(C3-e) The norming of the Gaussian branch is regularly varying of index 1/2: a_{⌊l n⌋} / a_n → l^{1/2}, for a_n = norming ν 2 n = √(n K(g_n) / 2).