Integrated tail of the Gaussian branch

The integrated-tail asymptotic is the B3-b result for the index-two branch. Ported from BGWLeaves/StableAnalysis/GaussianBranch.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

5. (B3-b) The integrated tail

theorem BGW.StableTrees.Attraction.GaussianBranch.integratedTail_div_tendsto {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hneg : ν {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 : ℝ) => (∫ (u : ℝ) in 0..x, ∫ (z : ℤ), max (↑z - u) 0 ∂ν) / (truncSecondMoment ν x / 2)) Filter.atTop (nhds 1)

(B3-b) Let ν be a probability law on ℤ with ν {z < -1} = 0 and finite mean, such that K = truncSecondMoment ν is slowly varying and unbounded. Then the integrated tail J(x) = ∫₀ˣ E[(Z - u)⁺] du (E[(Z-u)⁺] = ∫_u^∞ ν{z > v} dv, see integral_max_sub_eq_integral_tail) satisfies J(x) / (K(x)/2) → 1.

Use: for the Laplace transform ℓ(s) = E e^{-s Z} one has the exact identity ℓ(s) - 1 + m s = s² ∫₀^∞ e^{-su} E[(Z-u)⁺] du + (explicit atom at -1), so (via the Laplace–Karamata Abelian theorem applied to U = J) ℓ(s) - 1 + m s ~ s² J(1/s) ~ s² K(1/s) / 2 as s → 0+.

theorem BGW.StableTrees.Attraction.GaussianBranch.integratedTail_isEquivalent {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hneg : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hK : SlowlyVarying (truncSecondMoment ν)) (hKinf : Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ∫ (u : ℝ) in 0..x, ∫ (z : ℤ), max (↑z - u) 0 ∂ν) fun (x : ℝ) => truncSecondMoment ν x / 2

theorem BGW.StableTrees.Attraction.GaussianBranch.integral_max_sub_eq_integral_tail {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (u : ℝ) : ∫ (z : ℤ), max (↑z - u) 0 ∂ν = ∫ (v : ℝ) in Set.Ioi u, ν.real {z : ℤ | v < ↑z}

The excess E[(Z-u)⁺] equals the integrated tail ∫_u^∞ ν{z > v} dv.