Laplace continuity with existence for centered laws

If probability laws P n on ℝ have mean zero (and integrable identity) and E_{P n} exp(-λ x) → exp(λ ^ θ) for every λ > 0, then P n converges weakly to a probability law Q with E_Q exp(-λ x) = exp(λ ^ θ).

• Tightness: the identity |x| ≤ x + 2 exp(-x) together with mean zero bounds the first absolute moment by 2 E exp(-x), which is bounded along the sequence.
• Prokhorov (isCompact_closure_of_isTightMeasureSet) gives convergent subsequences. In any weakly convergent subsequence the Laplace transform passes to the limit: truncate exp(-s x) at height R, control the truncation error by E exp(-2 s x) / R, then use Fatou/monotone convergence in R.
• The Laplace transform determines the law (Scalar.limitLaw_unique), so every subsequential limit is the same and the whole sequence converges.

isStableAttracted_of_laplace_limit specializes to the centered scaled integer walk, using the Laplace identity of centeredScaledWalk. Ported from BGWLeaves/StableAnalysis/LaplaceContinuity.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

Passing the Laplace transform to a weak limit

theorem BGW.StableTrees.Attraction.LaplaceContinuity.laplace_eq_of_tendsto {θ : ℝ} {P : ℕ → MeasureTheory.ProbabilityMeasure ℝ} {Q : MeasureTheory.ProbabilityMeasure ℝ} (hPQ : Filter.Tendsto P Filter.atTop (nhds Q)) (hL : ∀ (s : ℝ), 0 < s → Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), Real.exp (-s * x) ∂↑(P n)) Filter.atTop (nhds (Real.exp (s ^ θ)))) {s : ℝ} (hs : 0 < s) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-s * x)) ↑Q ∧ ∫ (x : ℝ), Real.exp (-s * x) ∂↑Q = Real.exp (s ^ θ)

Weak limits of laws with convergent Laplace transforms inherit the limiting Laplace transform (the transforms are integrable under the limit).

Tightness from a uniform first-moment bound

Abstract Laplace continuity

theorem BGW.StableTrees.Attraction.LaplaceContinuity.exists_tendsto_of_laplace_tendsto {θ : ℝ} (hθ : 0 < θ) (P : ℕ → MeasureTheory.ProbabilityMeasure ℝ) (hint : ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (fun (x : ℝ) => x) ↑(P n)) (hmean : ∀ᶠ (n : ℕ) in Filter.atTop, ∫ (x : ℝ), x ∂↑(P n) = 0) (hL : ∀ (s : ℝ), 0 < s → Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), Real.exp (-s * x) ∂↑(P n)) Filter.atTop (nhds (Real.exp (s ^ θ)))) : ∃ (Q : MeasureTheory.ProbabilityMeasure ℝ), (∀ (s : ℝ), 0 < s → ∫ (x : ℝ), Real.exp (-s * x) ∂↑Q = Real.exp (s ^ θ)) ∧ Filter.Tendsto P Filter.atTop (nhds Q)

Centered Laplace continuity with existence. Let P n be probability laws on ℝ which are eventually integrable with mean zero and satisfy E_{P n} exp(-s x) → exp(s ^ θ) for every s > 0. Then P n converges weakly to a probability law Q with Laplace transform E_Q exp(-s x) = exp(s ^ θ). Finite negative exponential moments of P n (eventually) are automatic from the convergence of the Laplace transforms.

The centered scaled integer walk

theorem BGW.StableTrees.Attraction.LaplaceContinuity.centeredScaledWalk_integrable_id (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hν : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (m a : ℝ) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x) (TransformConvergence.centeredScaledWalk ν m a n)

The identity is integrable under the centered scaled walk.

theorem BGW.StableTrees.Attraction.LaplaceContinuity.isStableAttracted_of_laplace_limit (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hstep : ν {z : ℤ | z < -1} = 0) (hν : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {b : ℕ → ℝ} (hb : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → 0 < b n) (hL : ∀ (lam : ℝ), 0 < lam → Filter.Tendsto (fun (n : ℕ) => TransformConvergence.stepLaplace ν (lam / b n) ^ n * Real.exp (lam * ↑n * mean ν / b n)) Filter.atTop (nhds (Real.exp (lam ^ θ)))) : IsStableAttracted ν θ (mean ν) b

Attraction from the Laplace limit. Let ν be a step law on ℤ with ν {z < -1} = 0 and finite mean, and b eventually positive with stepLaplace ν (λ / b n) ^ n * exp (λ n mean ν / b n) → exp (λ ^ θ) for every λ > 0 (this is the Laplace transform of centeredScaledWalk ν (mean ν) (b n) n). Then ν is attracted to the spectrally positive stable law with this centering and norming b.

theorem BGW.StableTrees.Attraction.LaplaceContinuity.isStableAttracted_of_centered_laplace_limit (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hstep : ν {z : ℤ | z < -1} = 0) (hν : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {b : ℕ → ℝ} (hb : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → 0 < b n) (hL : ∀ (lam : ℝ), 0 < lam → Filter.Tendsto (fun (n : ℕ) => (TransformConvergence.stepLaplace ν (lam / b n) * Real.exp (lam / b n * mean ν)) ^ n) Filter.atTop (nhds (Real.exp (lam ^ θ)))) : IsStableAttracted ν θ (mean ν) b

The same, with the centered one-step Laplace transform ℓ(s) = stepLaplace ν s * exp (s * mean ν) raised to the power n.