Bridge, tail branch

μ[j,∞) = j^{-θ} L(j) with L slowly varying gives a normalized stable domain of attraction. The step law ν = stepLaw μ has a regularly varying strict tail (TailTransfer); for θ < 2 the canonical attraction D2(i) applies, for θ = 2 either the finite variance CLT of BGW or the Gaussian criterion D2(ii) (slow variation of the truncated second moment, B3-a). The canonical norming is monotone, so IsStableAttracted.exists_stableDomain repairs its first terms. Ported from BGWLeaves/StableAnalysis/StableDomainTail.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

theorem BGW.StableTrees.Attraction.memLp_offspring_of_integrable_sq {μ : PMF ℕ} (h : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) (stepLaw μ)) : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure

A finite second moment of the step law K - 1 gives a finite second moment of K.

theorem BGW.StableTrees.Attraction.exists_stableDomain_of_tail {μ : PMF ℕ} {θ : ℝ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hθ : 1 < θ ∧ θ ≤ 2) {L : ℝ → ℝ} (hmeas : Measurable L) (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) (htail : ∀ (j : ℕ), 1 ≤ j → (μ.toMeasure (Set.Ici j)).toReal = ↑j ^ (-θ) * L ↑j) : ∃ (a : ℕ → ℝ), StableDomain μ θ a

Bridge, tail branch: μ[j,∞) = j^{-θ}L(j) gives a normalized domain of attraction.