Documentation

TauCeti.Analysis.CompletelyMonotone.Stieltjes.Laplace

Stieltjes functions are the Laplace transforms of completely monotone functions #

The Stieltjes kernel factors through a second exponential integration,

(t + x)⁻¹ = ∫₀^∞ e^{-s(t + x)} ds = ∫₀^∞ e^{-ts} e^{-sx} ds,

so integrating it against a measure ν on ℝ≥0 and swapping the two integrations turns the Stieltjes transform of ν into the Laplace transform of the Laplace transform of ν. Since the Laplace transforms of measures on ℝ≥0 are exactly the functions completely monotone on (0, ∞) (TauCeti.hausdorff_bernstein_widder_onIoi), this identifies the Stieltjes functions:

a function is a Stieltjes function if and only if it is a nonnegative constant plus the Laplace transform of a function completely monotone on (0, ∞).

The additive constant is genuinely needed and cannot be absorbed: it is the coefficient b of the Stieltjes representation, whose "representing measure" is a point mass of the outer variable at 0, which no density supplies. The singular coefficient a of the Stieltjes formula, by contrast, is absorbed: it is the constant part of the completely monotone integrand, since a / t = ∫₀^∞ e^{-ts} a ds.

This is the converse half of the Stieltjes theory begun in TauCeti.Analysis.CompletelyMonotone.Stieltjes.CompletelyMonotone (a Stieltjes function is completely monotone) and TauCeti.Analysis.CompletelyMonotone.Stieltjes.Bernstein (the product with the parameter extends to a Bernstein function): those two run only from a Stieltjes representation outwards, whereas the equivalence below also produces one.

Main declarations #

References #

The exponential kernel against a Stieltjes weight #

source
theorem TauCeti.integrable_exp_neg_mul_of_integrable_stieltjesWeight {ν : MeasureTheory.Measure NNReal} (hν : MeasureTheory.Integrable stieltjesWeight ν) {t : ℝ} (ht : 0 < t) :
MeasureTheory.Integrable (fun (x : NNReal) => Real.exp (-(t * ↑x))) ν

The exponential kernel is integrable against every measure carrying an integrable Stieltjes weight: e^{-tx} ≤ (1 + tx)⁻¹ ≤ (min 1 t)⁻¹ (1 + x)⁻¹. Together with TauCeti.integrable_inv_add this says that a Stieltjes representing measure is also a Laplace representing measure.

The two transforms of a Laplace representing measure #

source
theorem TauCeti.RepresentsLaplaceOnIoi.lintegral_ofReal_exp_neg_mul_mul {ν : MeasureTheory.Measure NNReal} {g : ℝ → ℝ} (h : RepresentsLaplaceOnIoi ν g) {t : ℝ} (ht : 0 < t) :
∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-(t * s)) * g s) = ∫⁻ (x : NNReal), ENNReal.ofReal (t + ↑x)⁻¹ ∂ν

The Stieltjes transform is the iterated Laplace transform, in extended-real form: if ν represents g by its Laplace transform on (0, ∞), then the outer Laplace integral of g is the Stieltjes integral of ν. Both sides may be infinite.

source
theorem TauCeti.RepresentsLaplaceOnIoi.integrable_inv_add_of_integrableOn {ν : MeasureTheory.Measure NNReal} {g : ℝ → ℝ} (h : RepresentsLaplaceOnIoi ν g) {t : ℝ} (ht : 0 < t) (hint : MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.exp (-(t * s)) * g s) (Set.Ioi 0) MeasureTheory.volume) :
MeasureTheory.Integrable (fun (x : NNReal) => (t + ↑x)⁻¹) ν

Convergence of the outer Laplace integral forces the Stieltjes kernel to be integrable against the representing measure.

source
theorem TauCeti.RepresentsLaplaceOnIoi.integrableOn_exp_neg_mul_mul {ν : MeasureTheory.Measure NNReal} {g : ℝ → ℝ} (h : RepresentsLaplaceOnIoi ν g) {t : ℝ} (ht : 0 < t) (hint : MeasureTheory.Integrable (fun (x : NNReal) => (t + ↑x)⁻¹) ν) :
MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.exp (-(t * s)) * g s) (Set.Ioi 0) MeasureTheory.volume

Integrability of the Stieltjes kernel against the representing measure makes the outer Laplace integral converge.

source
theorem TauCeti.RepresentsLaplaceOnIoi.integral_exp_neg_mul_mul {ν : MeasureTheory.Measure NNReal} {g : ℝ → ℝ} (h : RepresentsLaplaceOnIoi ν g) {t : ℝ} (ht : 0 < t) (hint : MeasureTheory.Integrable (fun (x : NNReal) => (t + ↑x)⁻¹) ν) :
∫ (s : ℝ) in Set.Ioi 0, Real.exp (-(t * s)) * g s = ∫ (x : NNReal), (t + ↑x)⁻¹ ∂ν

The Stieltjes transform is the iterated Laplace transform. Bochner form of TauCeti.RepresentsLaplaceOnIoi.lintegral_ofReal_exp_neg_mul_mul.

Stieltjes functions from completely monotone integrands #

source
theorem TauCeti.isStieltjesFunction_const_add_integral_exp_neg_mul {g : ℝ → ℝ} (b : NNReal) (hg : IsCompletelyMonotoneOnIoi g) (hint : ∀ (t : ℝ), 0 < t → MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.exp (-(t * s)) * g s) (Set.Ioi 0) MeasureTheory.volume) :
IsStieltjesFunction fun (t : ℝ) => ↑b + ∫ (s : ℝ) in Set.Ioi 0, Real.exp (-(t * s)) * g s

A constant plus the Laplace transform of a completely monotone function is a Stieltjes function. The singular coefficient of the resulting Stieltjes representation is the mass that the representing measure of g puts at the origin.

Stieltjes representations as iterated Laplace transforms #

source
theorem TauCeti.RepresentsStieltjes.exists_isCompletelyMonotoneOnIoi {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} {a b : NNReal} (h : RepresentsStieltjes μ a b f) :
∃ (g : ℝ → ℝ), IsCompletelyMonotoneOnIoi g ∧ (∀ (t : ℝ), 0 < t → MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.exp (-(t * s)) * g s) (Set.Ioi 0) MeasureTheory.volume) ∧ ∀ (t : ℝ), 0 < t → f t = ↑b + ∫ (s : ℝ) in Set.Ioi 0, Real.exp (-(t * s)) * g s

A Stieltjes representation exhibits its function as a constant plus the Laplace transform of a completely monotone function. The completely monotone integrand is the singular coefficient plus the Laplace transform of the representing measure.

The characterization #

source
theorem TauCeti.isStieltjesFunction_iff_exists_isCompletelyMonotoneOnIoi {f : ℝ → ℝ} :
IsStieltjesFunction f ↔ ∃ (b : NNReal) (g : ℝ → ℝ), IsCompletelyMonotoneOnIoi g ∧ (∀ (t : ℝ), 0 < t → MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.exp (-(t * s)) * g s) (Set.Ioi 0) MeasureTheory.volume) ∧ ∀ (t : ℝ), 0 < t → f t = ↑b + ∫ (s : ℝ) in Set.Ioi 0, Real.exp (-(t * s)) * g s

Stieltjes functions are exactly the Laplace transforms of completely monotone functions, up to an additive nonnegative constant. The constant b cannot be absorbed into the integrand: its representing data in the outer variable is a point mass at 0, which no density supplies.

Compare TauCeti.IsStieltjesFunction.isCompletelyMonotoneOnIoi, which says that a Stieltjes function is itself completely monotone -- a strictly weaker conclusion, since a completely monotone function need not be Stieltjes.