Consequences of the Gaussian-smoothed converse

For infinite second moment, Fubini identifies H(s)/s as the Laplace transform of the squared-difference tail density. Karamata and monotone density recover regular variation of its integrated tail. A uniform capped-moment comparison transfers this to the original step; a second application of monotone density recovers its squared tail, or the truncated moment at the Gaussian boundary.

The finite second moment case is obtained directly by dominated convergence, without a Tauberian theorem or a calculation of the smoothing constant.

Main exports: rightTail_regularlyVarying, truncSecondMoment_slowlyVarying_unbounded, index_eq_two_of_integrable_sq, and smoothing_isEquivalent_variance. Ported from BGWLeaves/StableAnalysis/DomainCriterion.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

theorem BGW.StableTrees.Attraction.DomainCriterion.smoothing_quotient_bounds {s x : ℝ} (hs : 0 < s) : 0 ≤ (1 - Real.exp (-s * x ^ 2)) / s ∧ (1 - Real.exp (-s * x ^ 2)) / s ≤ x ^ 2

The elementary bound used to dominate the smoothing difference quotient.

theorem BGW.StableTrees.Attraction.DomainCriterion.smoothing_div_tendsto_secondMoment (ν : MeasureTheory.Measure ℤ) (hD : MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (GaussianSmoothing.symmetrizedLaw ν)) : Filter.Tendsto (fun (s : ℝ) => GaussianSmoothing.smoothing ν s / s) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : ℝ), x ^ 2 ∂GaussianSmoothing.symmetrizedLaw ν))

If the symmetrized law has a finite second moment, H(s)/s tends to it.

theorem BGW.StableTrees.Attraction.DomainCriterion.integrable_sq_symmetrizedLaw (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hsq : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (GaussianSmoothing.symmetrizedLaw ν)

Finite second moment is preserved by independent symmetrization.

theorem BGW.StableTrees.Attraction.DomainCriterion.secondMoment_symmetrizedLaw (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hsq : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : ∫ (x : ℝ), x ^ 2 ∂GaussianSmoothing.symmetrizedLaw ν = 2 * variance ν

The independent difference has second moment twice the original variance.

theorem BGW.StableTrees.Attraction.DomainCriterion.smoothing_div_tendsto_variance (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hsq : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : Filter.Tendsto (fun (s : ℝ) => GaussianSmoothing.smoothing ν s / s) (nhdsWithin 0 (Set.Ioi 0)) (nhds (2 * variance ν))

The finite-variance expansion, in a form that also includes the degenerate law.

theorem BGW.StableTrees.Attraction.DomainCriterion.smoothing_div_le_secondMoment (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hD : MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (GaussianSmoothing.symmetrizedLaw ν)) {s : ℝ} (hs : 0 < s) : GaussianSmoothing.smoothing ν s / s ≤ ∫ (x : ℝ), x ^ 2 ∂GaussianSmoothing.symmetrizedLaw ν

The smoothing is bounded above by its linear finite-moment majorant.

theorem BGW.StableTrees.Attraction.DomainCriterion.secondMoment_symmetrizedLaw_pos {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hD : MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (GaussianSmoothing.symmetrizedLaw ν)) : 0 < ∫ (x : ℝ), x ^ 2 ∂GaussianSmoothing.symmetrizedLaw ν

Attraction excludes a degenerate symmetrized second moment.

theorem BGW.StableTrees.Attraction.DomainCriterion.variance_pos_of_integrable_sq {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hsq : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : 0 < variance ν

A finite-variance law attracted to a stable law has positive variance.

theorem BGW.StableTrees.Attraction.DomainCriterion.index_eq_two_of_integrable_sq {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hsq : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : θ = 2

Finite second moment forces the Gaussian stable index. No support assumption is needed for this direction.

theorem BGW.StableTrees.Attraction.DomainCriterion.smoothing_isEquivalent_variance {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hsq : MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : Asymptotics.IsEquivalent (nhdsWithin 0 (Set.Ioi 0)) (GaussianSmoothing.smoothing ν) fun (s : ℝ) => 2 * variance ν * s

In the attracting finite-variance case the linear smoothing asymptotic is nonzero, hence it can also be stated as asymptotic equivalence.

theorem BGW.StableTrees.Attraction.DomainCriterion.smoothing_pos {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) {s : ℝ} (hs : 0 < s) : 0 < GaussianSmoothing.smoothing ν s

Every positive smoothing parameter has strictly positive defect under attraction.

theorem BGW.StableTrees.Attraction.DomainCriterion.smoothing_regularlyVaryingAtZero {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) : KaramataTransforms.RegularlyVaryingAtZero (GaussianSmoothing.smoothing ν) (θ / 2)

D3 in the positive, reciprocal-coordinate predicate expected by B1.

theorem BGW.StableTrees.Attraction.DomainCriterion.smoothing_quotient_regularlyVaryingAtZero {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) : KaramataTransforms.RegularlyVaryingAtZero (fun (s : ℝ) => GaussianSmoothing.smoothing ν s / s) (θ / 2 - 1)

Dividing the smoothing by its parameter gives the Laplace exponent needed for the integrated squared-difference tail, including the boundary exponent zero.

noncomputable def BGW.StableTrees.Attraction.DomainCriterion.squaredTail (ν : MeasureTheory.Measure ℤ) (y : ℝ) : ℝ

Tail of the squared independent difference.

Equations

• BGW.StableTrees.Attraction.DomainCriterion.squaredTail ν y = (BGW.StableTrees.Attraction.GaussianSmoothing.symmetrizedLaw ν).real {x : ℝ | y < x ^ 2}

theorem BGW.StableTrees.Attraction.DomainCriterion.squaredTail_antitone (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] : Antitone (squaredTail ν)

theorem BGW.StableTrees.Attraction.DomainCriterion.squaredTail_bounds (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (y : ℝ) : 0 ≤ squaredTail ν y ∧ squaredTail ν y ≤ 1

noncomputable def BGW.StableTrees.Attraction.DomainCriterion.squaredTailMeasure (ν : MeasureTheory.Measure ℤ) : MeasureTheory.Measure ℝ

Locally finite measure whose density is the squared-difference tail.

Equations

• BGW.StableTrees.Attraction.DomainCriterion.squaredTailMeasure ν = MeasureTheory.volume.withDensity fun (y : ℝ) => ENNReal.ofReal (BGW.StableTrees.Attraction.DomainCriterion.squaredTail ν y)

instance BGW.StableTrees.Attraction.DomainCriterion.squaredTailMeasure_locallyFinite (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsLocallyFiniteMeasure (squaredTailMeasure ν)

theorem BGW.StableTrees.Attraction.DomainCriterion.squaredTailMeasure_laplace_integrable (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {s : ℝ} (hs : 0 < s) : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) (squaredTailMeasure ν)

theorem BGW.StableTrees.Attraction.DomainCriterion.laplace_squaredTailMeasure (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {s : ℝ} (hs : 0 < s) : KaramataTransforms.laplace (squaredTailMeasure ν) s = GaussianSmoothing.smoothing ν s / s

The layer-cake/Fubini identity that turns D3 into the transform hypothesis of B1.

theorem BGW.StableTrees.Attraction.DomainCriterion.cumulative_squaredTailMeasure (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {y : ℝ} (hy : 0 ≤ y) : KaramataTransforms.cumulative (squaredTailMeasure ν) y = ∫ (t : ℝ) in 0..y, squaredTail ν t

The cumulative mass of the tail-density measure is the integrated tail.

theorem BGW.StableTrees.Attraction.DomainCriterion.integratedSquaredTail_regularlyVarying {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) : KaramataTransforms.RegularlyVarying (fun (y : ℝ) => ∫ (t : ℝ) in 0..y, squaredTail ν t) (1 - θ / 2)

The Tauberian output for the symmetrized squared step, valid also at index two.

theorem BGW.StableTrees.Attraction.DomainCriterion.squaredTail_density_limit {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) : Filter.Tendsto (fun (y : ℝ) => y * squaredTail ν y / ∫ (t : ℝ) in 0..y, squaredTail ν t) Filter.atTop (nhds (1 - θ / 2))

The monotone density conclusion, including its zero limit at the Gaussian boundary.

theorem BGW.StableTrees.Attraction.DomainCriterion.squaredTail_regularlyVarying {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hθ : θ < 2) : MonotoneDensity.IsRegVaryAtTop (squaredTail ν) (-θ / 2)

Below the Gaussian index, the squared-difference tail itself is regularly varying.

theorem BGW.StableTrees.Attraction.DomainCriterion.capped_difference_bound (a b x : ℝ) : |min ((a - b) ^ 2) (x ^ 2) - min (a ^ 2) (x ^ 2) - min (b ^ 2) (x ^ 2)| ≤ 2 * |a * b|

Uniform pointwise comparison of capped squared differences and capped squares.

theorem BGW.StableTrees.Attraction.DomainCriterion.integral_min_sq_eq_integrated_tail {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → ℝ) (hX : Measurable X) {y : ℝ} (hy : 0 ≤ y) : ∫ (ω : Ω), min (X ω ^ 2) y ∂μ = ∫ (t : ℝ) in 0..y, μ.real {ω : Ω | t < X ω ^ 2}

Layer cake for a capped square. This form needs no second-moment hypothesis.

noncomputable def BGW.StableTrees.Attraction.DomainCriterion.cappedSecondMoment (ν : MeasureTheory.Measure ℤ) (y : ℝ) : ℝ

Capped second moment, with the cutoff in squared coordinates.

Equations

• BGW.StableTrees.Attraction.DomainCriterion.cappedSecondMoment ν y = ∫ (z : ℤ), min (↑z ^ 2) y ∂ν

theorem BGW.StableTrees.Attraction.DomainCriterion.integratedSquaredTail_sub_two_capped_bound (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) {y : ℝ} (hy : 0 ≤ y) : |(∫ (t : ℝ) in 0..y, squaredTail ν t) - 2 * cappedSecondMoment ν y| ≤ 2 * (∫ (z : ℤ), |↑z| ∂ν) ^ 2

The bounded-error desymmetrization estimate.

theorem BGW.StableTrees.Attraction.DomainCriterion.truncSecondMoment_sqrt_le_capped (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {y : ℝ} (hy : 0 ≤ y) : truncSecondMoment ν √y ≤ cappedSecondMoment ν y

The truncated moment is dominated by the capped moment.

theorem BGW.StableTrees.Attraction.DomainCriterion.cappedSecondMoment_tendsto_atTop (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : Filter.Tendsto (cappedSecondMoment ν) Filter.atTop Filter.atTop

Infinite second moment forces the capped moments to diverge.

theorem BGW.StableTrees.Attraction.DomainCriterion.cappedSecondMoment_regularlyVarying {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : KaramataTransforms.RegularlyVarying (cappedSecondMoment ν) (1 - θ / 2)

Desymmetrization transfers the integrated-tail variation to the original capped moment.

noncomputable def BGW.StableTrees.Attraction.DomainCriterion.stepSquaredTail (ν : MeasureTheory.Measure ℤ) (y : ℝ) : ℝ

Tail of the square of the original step.

Equations

• BGW.StableTrees.Attraction.DomainCriterion.stepSquaredTail ν y = ν.real {z : ℤ | y < ↑z ^ 2}

theorem BGW.StableTrees.Attraction.DomainCriterion.stepSquaredTail_antitone (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] : Antitone (stepSquaredTail ν)

theorem BGW.StableTrees.Attraction.DomainCriterion.stepSquaredTail_density_limit {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : Filter.Tendsto (fun (y : ℝ) => y * stepSquaredTail ν y / cappedSecondMoment ν y) Filter.atTop (nhds (1 - θ / 2))

Monotone density for the original capped moments.

theorem BGW.StableTrees.Attraction.DomainCriterion.stepSquaredTail_regularlyVarying {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) (hθ : θ < 2) : MonotoneDensity.IsRegVaryAtTop (stepSquaredTail ν) (-θ / 2)

Below index two, monotone density identifies the tail of the original square.

theorem BGW.StableTrees.Attraction.DomainCriterion.stepSquaredTail_sq_eq_rightTail (ν : MeasureTheory.Measure ℤ) (hneg : ν {z : ℤ | z < -1} = 0) {x : ℝ} (hx : 1 ≤ x) : stepSquaredTail ν (x ^ 2) = ν.real {z : ℤ | x < ↑z}

Bounded negative support removes the negative contribution to the squared tail.

theorem BGW.StableTrees.Attraction.DomainCriterion.rightTail_regularlyVarying {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ (mean ν) b) (hneg : ν {z : ℤ | z < -1} = 0) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) (hθ : θ < 2) : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => ν.real {z : ℤ | x < ↑z}) (-θ)

D4, non-Gaussian branch: attraction with infinite second moment forces regular variation of the right tail with index -θ.

theorem BGW.StableTrees.Attraction.DomainCriterion.truncSecondMoment_sqrt_eq_capped_sub_tail (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {y : ℝ} (hy : 0 ≤ y) : truncSecondMoment ν √y = cappedSecondMoment ν y - y * stepSquaredTail ν y

Capped and truncated moments differ by the endpoint tail term.

theorem BGW.StableTrees.Attraction.DomainCriterion.truncSecondMoment_slowlyVarying_unbounded {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {b : ℕ → ℝ} (hb : IsStableAttracted ν 2 (mean ν) b) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hinf : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν) : SlowlyVarying (truncSecondMoment ν) ∧ Filter.Tendsto (truncSecondMoment ν) Filter.atTop Filter.atTop

D4, Gaussian branch: infinite second moment and Gaussian attraction imply slow variation and divergence of the truncated second moment. The proof needs no support bound, because the capped-moment comparison already handles both tails.

theorem BGW.StableTrees.Attraction.DomainCriterion.not_integrable_sq_of_index_lt_two {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (hint : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (hθ : θ < 2) : ¬MeasureTheory.Integrable (fun (z : ℤ) => ↑z ^ 2) ν

Stable attraction below index two automatically has infinite second moment.