Laplace transforms of convolutions, dilations and translations

The Laplace transform t ↦ ∫ e^{-tx} dμ(x) of a measure on ℝ≥0 turns the basic operations on measures into operations on functions:

• the additive convolution μ ∗ ν goes to the pointwise product of the transforms;
• the pushforward of μ along the dilation x ↦ c x goes to the reparametrization t ↦ L(c t);
• the pushforward of μ along the translation x ↦ x + p goes to the product with the exponential t ↦ e^{-tp}, the transform of the point mass at p.

Read through the predicate TauCeti.RepresentsLaplace, these say which finite measure represents a product of represented functions, a rescaled one, and one multiplied by an exponential. Together with the uniqueness of representing measures they identify the Bernstein measure of a product of completely monotone functions as the convolution of the two Bernstein measures.

Main declarations

• TauCeti.laplaceTransform_conv: the transform of μ ∗ ν is the product of the transforms.
• TauCeti.laplaceTransform_map_const_mul, TauCeti.laplaceTransform_map_add_const: the transforms of the dilated and translated measures.
• TauCeti.RepresentsLaplace.conv, TauCeti.RepresentsLaplace.comp_const_mul, TauCeti.RepresentsLaplace.exp_neg_mul_mul: the corresponding representation statements.

References

• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II (Wiley, 2nd ed. 1971), Chapter XIII, Section 2.
• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications (de Gruyter, 2nd ed. 2012), Corollary 1.6.

The Laplace transform of the basic measure operations

@[simp]

theorem TauCeti.laplaceTransform_conv (μ ν : MeasureTheory.Measure NNReal) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (t : ℝ) : laplaceTransform (μ.conv ν) t = laplaceTransform μ t * laplaceTransform ν t

The Laplace transform turns convolution into multiplication. The identity needs no finiteness or integrability hypothesis: under the junk-value convention for non-integrable Bochner integrals it holds for all s-finite measures and every real parameter t.

@[simp]

theorem TauCeti.laplaceTransform_map_const_mul (μ : MeasureTheory.Measure NNReal) (c : NNReal) (t : ℝ) : laplaceTransform (MeasureTheory.Measure.map (fun (x : NNReal) => c * x) μ) t = laplaceTransform μ (↑c * t)

Dilating a measure by c reparametrizes its Laplace transform by c.

@[simp]

theorem TauCeti.laplaceTransform_map_add_const (μ : MeasureTheory.Measure NNReal) (p : NNReal) (t : ℝ) : laplaceTransform (MeasureTheory.Measure.map (fun (x : NNReal) => x + p) μ) t = Real.exp (-(t * ↑p)) * laplaceTransform μ t

Translating a measure by p multiplies its Laplace transform by the exponential e^{-tp}.

Representing measures of products, dilations and exponential factors

theorem TauCeti.RepresentsLaplace.conv {f g : ℝ → ℝ} {μ ν : MeasureTheory.Measure NNReal} (hf : RepresentsLaplace μ f) (hg : RepresentsLaplace ν g) : RepresentsLaplace (μ.conv ν) (f * g)

The convolution of representing measures represents the product of the functions.

theorem TauCeti.RepresentsLaplace.comp_const_mul {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (hf : RepresentsLaplace μ f) (c : NNReal) : RepresentsLaplace (MeasureTheory.Measure.map (fun (x : NNReal) => c * x) μ) fun (t : ℝ) => f (↑c * t)

Dilating a representing measure by c represents the reparametrized function t ↦ f (c t).

theorem TauCeti.RepresentsLaplace.exp_neg_mul_mul {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (hf : RepresentsLaplace μ f) (p : NNReal) : RepresentsLaplace (MeasureTheory.Measure.map (fun (x : NNReal) => x + p) μ) fun (t : ℝ) => Real.exp (-(t * ↑p)) * f t

Translating a representing measure by p represents the function multiplied by the exponential t ↦ e^{-tp}.