Restricted Laplace–Stieltjes Karamata theorem

RegularlyVarying U ρ means eventual strict positivity and convergence of U (c*x) / U x to c^ρ at infinity, for every c > 0. The reciprocal parameterization x ↦ F (1/x) will be used for variation at zero.

The cumulative function includes the atom at zero. All transforms are restricted to the nonnegative half line; mass on the negative half line is irrelevant.

laplace_karamata proves both directions for 0 ≤ ρ < 1; laplace_karamata_normalization gives the exact Gamma constant. The Abelian proof uses monotonicity, doubling, and an exponential majorant. The Tauberian proof exponentially tilts and compactifies, uses polynomial approximation, and sandwiches the bounded discontinuous cutoff between continuous functions. The index-zero limit is an atom and is handled separately. Ported from BGWLeaves/StableAnalysis/KaramataTransforms.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

def BGW.StableTrees.Attraction.KaramataTransforms.RegularlyVarying (U : ℝ → ℝ) (ρ : ℝ) : Prop

Function regular variation at infinity, including eventual positivity.

Equations

• One or more equations did not get rendered due to their size.

def BGW.StableTrees.Attraction.KaramataTransforms.RegularlyVaryingAtZero (F : ℝ → ℝ) (κ : ℝ) : Prop

Regular variation at zero through reciprocal parameterization. Equivalently, the ratios F (c*s) / F s converge to c^κ as s decreases to zero.

Equations

• BGW.StableTrees.Attraction.KaramataTransforms.RegularlyVaryingAtZero F κ = BGW.StableTrees.Attraction.KaramataTransforms.RegularlyVarying (fun (x : ℝ) => F (1 / x)) (-κ)

noncomputable def BGW.StableTrees.Attraction.KaramataTransforms.cumulative (M : MeasureTheory.Measure ℝ) (x : ℝ) : ℝ

The cumulative mass, including the possible atom at zero.

Equations

• BGW.StableTrees.Attraction.KaramataTransforms.cumulative M x = M.real (Set.Icc 0 x)

noncomputable def BGW.StableTrees.Attraction.KaramataTransforms.laplace (M : MeasureTheory.Measure ℝ) (s : ℝ) : ℝ

The Laplace–Stieltjes transform on the nonnegative half line. Its use as a finite transform requires integrability, not just a value of this total integral.

Equations

• BGW.StableTrees.Attraction.KaramataTransforms.laplace M s = ∫ (y : ℝ) in Set.Ici 0, Real.exp (-s * y) ∂M

theorem BGW.StableTrees.Attraction.KaramataTransforms.regularlyVarying_zero_iff {U : ℝ → ℝ} : RegularlyVarying U 0 ↔ (∀ᶠ (x : ℝ) in Filter.atTop, 0 < U x) ∧ SlowlyVarying U

theorem BGW.StableTrees.Attraction.KaramataTransforms.cumulative_nonneg (M : MeasureTheory.Measure ℝ) (x : ℝ) : 0 ≤ cumulative M x

theorem BGW.StableTrees.Attraction.KaramataTransforms.cumulative_monotone (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] : Monotone (cumulative M)

theorem BGW.StableTrees.Attraction.KaramataTransforms.RegularlyVarying.eventually_doubling_le {U : ℝ → ℝ} {ρ : ℝ} (h : RegularlyVarying U ρ) (hρ : ρ < 1) : ∀ᶠ (x : ℝ) in Filter.atTop, U (2 * x) ≤ 2 * U x

Below index one, doubling can eventually be bounded by the factor two. This bound is intentionally coarse: it gives exponential domination directly.

theorem BGW.StableTrees.Attraction.KaramataTransforms.ratio_le_exp_of_doubling {U : ℝ → ℝ} (hmono : Monotone U) {X x : ℝ} (hdouble : ∀ (y : ℝ), X ≤ y → U (2 * y) ≤ 2 * U y) (hxX : X ≤ x) (hx : 0 < x) (hUx : 0 < U x) {t : ℝ} (ht : 0 ≤ t) : U (t * x) / U x ≤ Real.exp (Real.log 2 * t)

Monotonicity and a doubling bound give a single integrable exponential majorant for the Abelian rescaling.

theorem BGW.StableTrees.Attraction.KaramataTransforms.cumulative_integral_limit {U : ℝ → ℝ} {ρ : ℝ} (hnonneg : ∀ (x : ℝ), 0 ≤ U x) (hmono : Monotone U) (h : RegularlyVarying U ρ) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t) * (U (t * x) / U x)) Filter.atTop (nhds (Real.Gamma (1 + ρ)))

Abelian dominated convergence for the cumulative integral. This includes ρ = 0; the limiting integrand is then just the exponential density.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_eq_cumulative_integral (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {s : ℝ} (hs : 0 < s) (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) : laplace M s = s * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-s * t) * cumulative M t

Fubini's cumulative-integral formula, with the atom at zero retained.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_reciprocal_eq (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {x : ℝ} (hx : 0 < x) (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-(1 / x) * y)) (Set.Ici 0) M) : laplace M (1 / x) = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t) * cumulative M (t * x)

Change of variables in the cumulative-integral formula.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_abelian_ratio (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hU : RegularlyVarying (cumulative M) ρ) : Filter.Tendsto (fun (x : ℝ) => laplace M (1 / x) / cumulative M x) Filter.atTop (nhds (Real.Gamma (1 + ρ)))

Abelian half of the restricted Laplace–Stieltjes Karamata theorem, including its exact Gamma constant and the endpoint index zero.

theorem BGW.StableTrees.Attraction.KaramataTransforms.RegularlyVarying.of_ratio {U V : ℝ → ℝ} {ρ C : ℝ} (hU : RegularlyVarying U ρ) (hC : 0 < C) (hVU : Filter.Tendsto (fun (x : ℝ) => V x / U x) Filter.atTop (nhds C)) : RegularlyVarying V ρ

Regular variation is preserved by a strictly positive asymptotic multiplier.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_abelian (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hU : RegularlyVarying (cumulative M) ρ) : RegularlyVaryingAtZero (laplace M) (-ρ)

The Abelian regular-variation conclusion at zero.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_abelian_normalization (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hU : RegularlyVarying (cumulative M) ρ) : Filter.Tendsto (fun (x : ℝ) => cumulative M x / (laplace M (1 / x) / Real.Gamma (1 + ρ))) Filter.atTop (nhds 1)

Exact normalization, in the ratio-one form of asymptotic equivalence.

theorem BGW.StableTrees.Attraction.KaramataTransforms.tendsto_functional_of_monomials {ι : Type u_1} {l : Filter ι} {K : Set ℝ} [CompactSpace ↑K] (L : ι → C(↑K, ℝ) →L[ℝ] ℝ) (L₀ : C(↑K, ℝ) →L[ℝ] ℝ) (hbound : ∀ (i : ι), ‖L i‖ ≤ 1) (hmom : ∀ (n : ℕ), Filter.Tendsto (fun (i : ι) => (L i) (ContinuousMap.restrict K (ContinuousMap.id ℝ) ^ n)) l (nhds (L₀ (ContinuousMap.restrict K (ContinuousMap.id ℝ) ^ n)))) (f : C(↑K, ℝ)) : Filter.Tendsto (fun (i : ι) => (L i) f) l (nhds (L₀ f))

The polynomial-approximation step of the Tauberian argument. Uniformly bounded linear functionals on a compact real set converge on every continuous function as soon as they converge on all monomials.

theorem BGW.StableTrees.Attraction.KaramataTransforms.tilted_monomial_integral (M : MeasureTheory.Measure ℝ) (s : ℝ) (n : ℕ) : ∫ (y : ℝ) in Set.Ici 0, Real.exp (-s * y) * Real.exp (-s * y) ^ n ∂M = laplace M ((↑n + 1) * s)

Monomials after exponential tilting are Laplace transforms at integer multiples of the parameter. This identity does not require a limiting argument.

theorem BGW.StableTrees.Attraction.KaramataTransforms.tilted_monomial_limit (M : MeasureTheory.Measure ℝ) {ρ : ℝ} (hF : RegularlyVaryingAtZero (laplace M) (-ρ)) (n : ℕ) : Filter.Tendsto (fun (x : ℝ) => (∫ (y : ℝ) in Set.Ici 0, Real.exp (-(1 / x) * y) * Real.exp (-(1 / x) * y) ^ n ∂M) / laplace M (1 / x)) Filter.atTop (nhds ((1 / (↑n + 1)) ^ ρ))

Transform regular variation supplies all moments needed after exponential tilting and the substitution t = exp (-y/x).

noncomputable def BGW.StableTrees.Attraction.KaramataTransforms.expUnit (y : ℝ) : ↑(Set.Icc 0 1)

Exponential compactification. The extension to negative arguments makes this a continuous map on the whole real line. On nonnegative arguments it is exactly y ↦ exp (-y).

Equations

• BGW.StableTrees.Attraction.KaramataTransforms.expUnit y = ⟨Real.exp (-max 0 y), ⋯⟩

theorem BGW.StableTrees.Attraction.KaramataTransforms.continuous_expUnit : Continuous expUnit

theorem BGW.StableTrees.Attraction.KaramataTransforms.expUnit_coe {y : ℝ} (hy : 0 ≤ y) : ↑(expUnit y) = Real.exp (-y)

theorem BGW.StableTrees.Attraction.KaramataTransforms.tilted_test_integrable (M : MeasureTheory.Measure ℝ) {s : ℝ} (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (f : C(↑(Set.Icc 0 1), ℝ)) : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y) * f (expUnit (s * y))) (Set.Ici 0) M

noncomputable def BGW.StableTrees.Attraction.KaramataTransforms.tiltedFunctional (M : MeasureTheory.Measure ℝ) {s : ℝ} (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hpos : 0 < laplace M s) : C(↑(Set.Icc 0 1), ℝ) →L[ℝ] ℝ

The normalized exponentially tilted integral, as a bounded linear functional on the compact interval.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.Attraction.KaramataTransforms.tiltedFunctional_apply (M : MeasureTheory.Measure ℝ) {s : ℝ} (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hpos : 0 < laplace M s) (f : C(↑(Set.Icc 0 1), ℝ)) : (tiltedFunctional M hfinite hpos) f = (∫ (y : ℝ) in Set.Ici 0, Real.exp (-s * y) * f (expUnit (s * y)) ∂M) / laplace M s

theorem BGW.StableTrees.Attraction.KaramataTransforms.tiltedFunctional_norm_le (M : MeasureTheory.Measure ℝ) {s : ℝ} (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hpos : 0 < laplace M s) : ‖tiltedFunctional M hfinite hpos‖ ≤ 1

theorem BGW.StableTrees.Attraction.KaramataTransforms.tiltedFunctional_nonneg (M : MeasureTheory.Measure ℝ) {s : ℝ} (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hpos : 0 < laplace M s) {f : C(↑(Set.Icc 0 1), ℝ)} (hf : ∀ (t : ↑(Set.Icc 0 1)), 0 ≤ f t) : 0 ≤ (tiltedFunctional M hfinite hpos) f

theorem BGW.StableTrees.Attraction.KaramataTransforms.tiltedFunctional_mono (M : MeasureTheory.Measure ℝ) {s : ℝ} (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hpos : 0 < laplace M s) {f g : C(↑(Set.Icc 0 1), ℝ)} (hfg : ∀ (t : ↑(Set.Icc 0 1)), f t ≤ g t) : (tiltedFunctional M hfinite hpos) f ≤ (tiltedFunctional M hfinite hpos) g

theorem BGW.StableTrees.Attraction.KaramataTransforms.tiltedFunctional_monomial (M : MeasureTheory.Measure ℝ) {s : ℝ} (hs : 0 ≤ s) (hfinite : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hpos : 0 < laplace M s) (n : ℕ) : (tiltedFunctional M hfinite hpos) (ContinuousMap.restrict (Set.Icc 0 1) (ContinuousMap.id ℝ) ^ n) = laplace M ((↑n + 1) * s) / laplace M s

theorem BGW.StableTrees.Attraction.KaramataTransforms.gamma_monomial_integral {ρ : ℝ} (hρ : 0 < ρ) (n : ℕ) : ∫ (y : ℝ) in Set.Ioi 0, Real.exp (-y) * Real.exp (-y) ^ n * y ^ (ρ - 1) / Real.Gamma ρ = (1 / (↑n + 1)) ^ ρ

The Gamma model has exactly the tilted moments prescribed by transform regular variation. The index-zero model is instead the atom at 1.

theorem BGW.StableTrees.Attraction.KaramataTransforms.gamma_cutoff_integral {ρ : ℝ} (hρ : 0 < ρ) : ∫ (y : ℝ) in Set.Icc 0 1, y ^ (ρ - 1) / Real.Gamma ρ = 1 / Real.Gamma (1 + ρ)

The value of the de-tilted Gamma cutoff, including its normalization.

noncomputable def BGW.StableTrees.Attraction.KaramataTransforms.cutoffBound : ℝ

A universal constant for the index-zero cutoff estimate.

Equations

• BGW.StableTrees.Attraction.KaramataTransforms.cutoffBound = max (Real.exp 1) (1 / (1 - Real.exp (-1)))

theorem BGW.StableTrees.Attraction.KaramataTransforms.cumulative_laplace_bound (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {x : ℝ} (hx : 0 < x) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) : |cumulative M x - laplace M (1 / x)| ≤ cutoffBound * (laplace M (1 / x) - laplace M (2 * (1 / x)))

A quantitative Tauberian estimate at index zero: the cumulative mass is controlled by the first two Laplace transforms.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_tauberian_zero_ratio (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hF : RegularlyVaryingAtZero (laplace M) 0) : Filter.Tendsto (fun (x : ℝ) => cumulative M x / laplace M (1 / x)) Filter.atTop (nhds 1)

The Tauberian ratio theorem at the boundary index zero. Concentration of the tilted law follows from its first moment, so no Gamma density is needed.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_tauberian_zero (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hF : RegularlyVaryingAtZero (laplace M) 0) : RegularlyVarying (cumulative M) 0

The Tauberian regular-variation conclusion at index zero.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_karamata_zero (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) : RegularlyVaryingAtZero (laplace M) 0 ↔ RegularlyVarying (cumulative M) 0

Both directions of the Laplace–Stieltjes Karamata theorem at index zero.

theorem BGW.StableTrees.Attraction.KaramataTransforms.tilted_continuous_test_limit (M : MeasureTheory.Measure ℝ) {ρ : ℝ} (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hF : RegularlyVaryingAtZero (laplace M) (-ρ)) (L₀ : C(↑(Set.Icc 0 1), ℝ) →L[ℝ] ℝ) (hmodel : ∀ (n : ℕ), L₀ (ContinuousMap.restrict (Set.Icc 0 1) (ContinuousMap.id ℝ) ^ n) = (1 / (↑n + 1)) ^ ρ) (f : C(↑(Set.Icc 0 1), ℝ)) : Filter.Tendsto (fun (x : ℝ) => (∫ (y : ℝ) in Set.Ici 0, Real.exp (-(1 / x) * y) * f (expUnit (1 / x * y)) ∂M) / laplace M (1 / x)) Filter.atTop (nhds (L₀ f))

Continuous-test convergence for exponentially tilted laws, once the model functional with Gamma moments has been specified. The model is a bounded linear functional, not an assumption about the cumulative function or its limit.

noncomputable def BGW.StableTrees.Attraction.KaramataTransforms.powerMeasure (ρ : ℝ) : MeasureTheory.Measure ℝ

The power-law model measure, whose Laplace transform is s^(-ρ). Only its nonnegative restriction is used.

Equations

• BGW.StableTrees.Attraction.KaramataTransforms.powerMeasure ρ = MeasureTheory.volume.withDensity fun (y : ℝ) => ENNReal.ofReal (y ^ (ρ - 1) / Real.Gamma ρ)

theorem BGW.StableTrees.Attraction.KaramataTransforms.powerMeasure_integrable {ρ s : ℝ} (hρ : 0 < ρ) (hs : 0 < s) : MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) (powerMeasure ρ)

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_powerMeasure {ρ s : ℝ} (hρ : 0 < ρ) (hs : 0 < s) : laplace (powerMeasure ρ) s = (1 / s) ^ ρ

noncomputable def BGW.StableTrees.Attraction.KaramataTransforms.gammaFunctional {ρ : ℝ} (hρ : 0 < ρ) : C(↑(Set.Icc 0 1), ℝ) →L[ℝ] ℝ

The Gamma model functional for a strictly positive index.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.Attraction.KaramataTransforms.gammaFunctional_monomial {ρ : ℝ} (hρ : 0 < ρ) (n : ℕ) : (gammaFunctional hρ) (ContinuousMap.restrict (Set.Icc 0 1) (ContinuousMap.id ℝ) ^ n) = (1 / (↑n + 1)) ^ ρ

theorem BGW.StableTrees.Attraction.KaramataTransforms.tilted_gamma_limit (M : MeasureTheory.Measure ℝ) {ρ : ℝ} (hρ : 0 < ρ) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hF : RegularlyVaryingAtZero (laplace M) (-ρ)) (f : C(↑(Set.Icc 0 1), ℝ)) : Filter.Tendsto (fun (x : ℝ) => (∫ (y : ℝ) in Set.Ici 0, Real.exp (-(1 / x) * y) * f (expUnit (1 / x * y)) ∂M) / laplace M (1 / x)) Filter.atTop (nhds ((gammaFunctional hρ) f))

The positive-index Tauberian argument up to continuous test functions: the tilted laws converge to the explicit Gamma model.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_tauberian_pos_ratio (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ : 0 < ρ) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hF : RegularlyVaryingAtZero (laplace M) (-ρ)) : Filter.Tendsto (fun (x : ℝ) => cumulative M x / laplace M (1 / x)) Filter.atTop (nhds (1 / Real.Gamma (1 + ρ)))

The positive-index Tauberian ratio theorem. The continuous approximations to the exponentially compactified cutoff are squeezed against the Gamma law.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_tauberian_ratio (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ : 0 ≤ ρ) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hF : RegularlyVaryingAtZero (laplace M) (-ρ)) : Filter.Tendsto (fun (x : ℝ) => cumulative M x / laplace M (1 / x)) Filter.atTop (nhds (1 / Real.Gamma (1 + ρ)))

Tauberian ratio theorem for every nonnegative index, including the atom which arises in the Gamma-model limit at index zero.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_tauberian (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ : 0 ≤ ρ) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hF : RegularlyVaryingAtZero (laplace M) (-ρ)) : RegularlyVarying (cumulative M) ρ

Tauberian regular variation of the cumulative mass.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_karamata (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) : RegularlyVaryingAtZero (laplace M) (-ρ) ↔ RegularlyVarying (cumulative M) ρ

Restricted Laplace–Stieltjes Karamata theorem. In reciprocal coordinates both functions have index ρ at infinity; the transform itself has index -ρ at zero. Eventual positivity in the regular-variation predicates excludes the zero measure on the nonnegative half line.

theorem BGW.StableTrees.Attraction.KaramataTransforms.laplace_karamata_normalization (M : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure M] {ρ : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hfinite : ∀ (s : ℝ), 0 < s → MeasureTheory.IntegrableOn (fun (y : ℝ) => Real.exp (-s * y)) (Set.Ici 0) M) (hF : RegularlyVaryingAtZero (laplace M) (-ρ)) : Filter.Tendsto (fun (x : ℝ) => cumulative M x / (laplace M (1 / x) / Real.Gamma (1 + ρ))) Filter.atTop (nhds 1)

The asymptotic normalization under the transform-side hypothesis.