Laplace representations for completely monotone functions

This file contains Laplace-representation infrastructure for completely monotone functions: helper lemmas for Laplace transforms, the predicate that a finite measure represents a function on [0, ∞), and its possibly infinite-measure counterpart on (0, ∞).

Main declarations

• TauCeti.laplaceTransform: the Laplace transform of a measure on ℝ≥0, with its algebraic API and the bridge TauCeti.laplaceTransform_eq_mgf to Mathlib's moment-generating function.
• TauCeti.measure_compl_closedBall_le_sub_laplaceTransform_div: a Markov tail bound, controlling the mass a finite measure puts far from the origin by the gap between its total mass and its Laplace transform at a positive parameter.
• TauCeti.RepresentsLaplace: the predicate that a finite measure represents a function by its Laplace transform on [0, ∞), with congr/add/smul/unique API.
• TauCeti.representsLaplace_laplaceTransformENN: every finite measure on ℝ≥0 is represented by its extended-real Laplace transform, after taking real values; conversely, TauCeti.RepresentsLaplace.laplaceTransformENN_eq recovers that extended-real transform.
• TauCeti.RepresentsLaplaceOnIoi: the corresponding predicate for a possibly infinite measure on (0, ∞), with its basic API and the easy direction of the representation theorem.
• TauCeti.isContinuousCompletelyMonotoneOnIoi_laplaceTransform, TauCeti.isCompletelyMonotone_laplaceTransform_of_moments: the easy direction of the representation theorem, in the closed-half-line and all-moments forms.
• TauCeti.Measure.ext_of_forall_laplaceTransform_natCast_eq: finite measures are determined by their Laplace transforms at the natural numbers.

References

The finite-measure representation is the Hausdorff--Bernstein--Widder theorem, after S. Bernstein (1928) and D. V. Widder, The Laplace Transform, Chapter IV; see also R. Schilling, R. Song, Z. Vondraček, Bernstein Functions (de Gruyter, 2nd ed. 2012), Theorem 1.4. This file provides the Laplace-transform API used by the representation theorem.

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B (Bernstein theorem milestone).

Laplace transforms of finite measures on ℝ≥0

noncomputable def TauCeti.laplaceTransform (μ : MeasureTheory.Measure NNReal) (t : ℝ) : ℝ

The Laplace transform of a measure on ℝ≥0, evaluated at a real parameter t.

The theorem statements in this file use the transform only for 0 ≤ t; for negative t, the Bochner integral is still a total Lean term, but may be the default value when the integrand is not integrable.

Equations

• TauCeti.laplaceTransform μ t = ∫ (x : NNReal), Real.exp (-(t * ↑x)) ∂μ

theorem TauCeti.laplaceTransform_apply (μ : MeasureTheory.Measure NNReal) (t : ℝ) : laplaceTransform μ t = ∫ (x : NNReal), Real.exp (-(t * ↑x)) ∂μ

The defining formula for laplaceTransform. Not @[simp]: simp should not unfold the abstraction into a raw integral; the evaluation lemmas below are the simp normal forms.

theorem TauCeti.laplaceTransform_eq_mgf (μ : MeasureTheory.Measure NNReal) : laplaceTransform μ = ProbabilityTheory.mgf (fun (p : NNReal) => -↑p) μ

The Laplace transform is the moment-generating function of the coordinate negation p ↦ -p on ℝ≥0. This bridge lets the transform consume Mathlib's mgf calculus.

@[simp]

theorem TauCeti.laplaceTransform_zero (μ : MeasureTheory.Measure NNReal) : laplaceTransform μ 0 = μ.real Set.univ

The value of the Laplace transform at the parameter 0 is the total mass (under the total Bochner-integral convention both sides are 0 for an infinite measure).

@[simp]

theorem TauCeti.laplaceTransform_zero_measure (t : ℝ) : laplaceTransform 0 t = 0

The Laplace transform of the zero measure vanishes identically.

theorem TauCeti.laplaceTransform_nonneg (μ : MeasureTheory.Measure NNReal) (t : ℝ) : 0 ≤ laplaceTransform μ t

The Laplace transform of a positive measure is nonnegative.

theorem TauCeti.laplaceTransform_add_measure (μ ν : MeasureTheory.Measure NNReal) {t : ℝ} (hμ : MeasureTheory.Integrable (fun (p : NNReal) => Real.exp (-(t * ↑p))) μ) (hν : MeasureTheory.Integrable (fun (p : NNReal) => Real.exp (-(t * ↑p))) ν) : laplaceTransform (μ + ν) t = laplaceTransform μ t + laplaceTransform ν t

Additivity of the Laplace transform in the measure, wherever the kernel is integrable against both summands.

theorem TauCeti.laplaceTransform_smul_measure (c : ENNReal) (μ : MeasureTheory.Measure NNReal) (t : ℝ) : laplaceTransform (c • μ) t = c.toReal * laplaceTransform μ t

Scaling the measure scales the Laplace transform by c.toReal. Unconditional in c : ℝ≥0∞: at c = ∞ both sides degenerate to 0, the Bochner integral over the infinite scalar multiple vanishing together with ∞.toReal.

@[simp]

theorem TauCeti.laplaceTransform_dirac (x₀ : NNReal) (t : ℝ) : laplaceTransform (MeasureTheory.Measure.dirac x₀) t = Real.exp (-(t * ↑x₀))

The Laplace transform of the Dirac mass at x₀ is the exponential kernel exp (-(t · x₀)); the point masses are the building blocks of the representing mixtures.

A Markov tail bound through the Laplace transform

theorem TauCeti.measure_compl_closedBall_le_sub_laplaceTransform_div (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] {x R : ℝ} (hx : 0 < x) (hR : 0 < R) : μ (Metric.closedBall 0 R)ᶜ ≤ ENNReal.ofReal ((μ.real Set.univ - laplaceTransform μ x) / (1 - Real.exp (-(x * R))))

A Markov tail bound through the Laplace transform. For a finite measure on ℝ≥0 and positive parameters x and R, the mass outside the closed ball of radius R is at most the Laplace gap μ.real univ - laplaceTransform μ x divided by 1 - e^{-xR}.

This is Markov's inequality applied to the bounded coordinate p ↦ 1 - e^{-xp}, which is at least 1 - e^{-xR} outside the ball. It is a tightness input rather than a decay rate in R: the denominator only tends to 1 as R → ∞, and it is the numerator, made small by taking x small, that does the work.

Easy direction: finite measures give completely monotone Laplace transforms

theorem TauCeti.continuousOn_Ici_laplaceTransform (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] : ContinuousOn (laplaceTransform μ) (Set.Ici 0)

The Laplace transform of a finite measure on ℝ≥0 is continuous on [0, ∞).

theorem TauCeti.contDiffOn_Ici_laplaceTransform_of_moments (μ : MeasureTheory.Measure NNReal) (hmom : ∀ (n : ℕ), MeasureTheory.Integrable (fun (x : NNReal) => ↑x ^ n) μ) : ContDiffOn ℝ (↑⊤) (laplaceTransform μ) (Set.Ici 0)

If all moments of the representing measure are finite, its Laplace transform is smooth on the closed half-line in the existing iteratedDerivWithin sense.

theorem TauCeti.contDiffOn_Ioi_laplaceTransform (μ : MeasureTheory.Measure NNReal) (hint : ∀ (t : ℝ), 0 < t → MeasureTheory.Integrable (fun (p : NNReal) => Real.exp (-(t * ↑p))) μ) : ContDiffOn ℝ (↑⊤) (laplaceTransform μ) (Set.Ioi 0)

A finite-measure Laplace transform is smooth on the open half-line: it is the moment-generating function of p ↦ -p, which is analytic on the interior of its integrability set.

theorem TauCeti.isCompletelyMonotoneOnIoi_laplaceTransform (μ : MeasureTheory.Measure NNReal) (hint : ∀ (t : ℝ), 0 < t → MeasureTheory.Integrable (fun (p : NNReal) => Real.exp (-(t * ↑p))) μ) : IsCompletelyMonotoneOnIoi (laplaceTransform μ)

Every finite-measure Laplace transform is completely monotone on (0, ∞).

theorem TauCeti.isContinuousCompletelyMonotoneOnIoi_laplaceTransform (μ : MeasureTheory.Measure NNReal) [hμ : MeasureTheory.IsFiniteMeasure μ] : IsContinuousCompletelyMonotoneOnIoi (laplaceTransform μ)

The Laplace transform of a finite measure is completely monotone in the closed-half-line roadmap sense.

theorem TauCeti.isCompletelyMonotone_laplaceTransform_of_moments (μ : MeasureTheory.Measure NNReal) (hmom : ∀ (n : ℕ), MeasureTheory.Integrable (fun (x : NNReal) => ↑x ^ n) μ) : IsCompletelyMonotone (laplaceTransform μ)

Strong easy direction: with all moments finite, the Laplace transform satisfies the existing IsCompletelyMonotone predicate using derivatives within [0, ∞).

Representation predicate

def TauCeti.RepresentsLaplace (μ : MeasureTheory.Measure NNReal) (f : ℝ → ℝ) : Prop

A finite measure represents a function by its Laplace transform on the nonnegative half-line.

Equations

• TauCeti.RepresentsLaplace μ f = (MeasureTheory.IsFiniteMeasure μ ∧ ∀ (t : ℝ), 0 ≤ t → f t = TauCeti.laplaceTransform μ t)

theorem TauCeti.representsLaplace_iff {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} : RepresentsLaplace μ f ↔ MeasureTheory.IsFiniteMeasure μ ∧ ∀ (t : ℝ), 0 ≤ t → f t = laplaceTransform μ t

RepresentsLaplace μ f unfolds to finiteness of μ and equality with the Laplace transform on the nonnegative half-line.

theorem TauCeti.RepresentsLaplace.isFiniteMeasure {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplace μ f) : MeasureTheory.IsFiniteMeasure μ

A representing measure is finite.

theorem TauCeti.RepresentsLaplace.eq_laplaceTransform {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplace μ f) {t : ℝ} (ht : 0 ≤ t) : f t = laplaceTransform μ t

A representing measure has the advertised Laplace-transform values on [0, ∞).

theorem TauCeti.RepresentsLaplace.apply_zero {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplace μ f) : f 0 = μ.real Set.univ

A represented function's value at 0 is the total mass of the representing measure. (Not @[simp]: the left-hand side f 0 has a variable head symbol.)

theorem TauCeti.RepresentsLaplace.isContinuousCompletelyMonotoneOnIoi {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplace μ f) : IsContinuousCompletelyMonotoneOnIoi f

A represented function is continuous on [0, ∞) and completely monotone on (0, ∞): the easy direction of the Hausdorff--Bernstein--Widder theorem, through the representation.

theorem TauCeti.RepresentsLaplace.congr {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} {g : ℝ → ℝ} (hf : RepresentsLaplace μ f) (h : Set.EqOn g f (Set.Ici 0)) : RepresentsLaplace μ g

A representation transports along agreement on the nonnegative half-line: the predicate constrains f only there.

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

The sum of two representing measures represents the sum of the functions.

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

Scaling a representing measure by c : ℝ≥0 represents the scaled function.

The real and extended-real Laplace transforms

theorem TauCeti.toReal_laplaceTransformENN (μ : MeasureTheory.Measure NNReal) (t : NNReal) [MeasureTheory.IsFiniteMeasure μ] : (laplaceTransformENN μ t).toReal = laplaceTransform μ ↑t

The real value of the extended-real Laplace transform of a finite measure is its usual Laplace transform.

theorem TauCeti.representsLaplace_laplaceTransformENN (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] : RepresentsLaplace μ fun (t : ℝ) => (laplaceTransformENN μ t.toNNReal).toReal

A finite measure is represented by its extended-real Laplace transform.

theorem TauCeti.RepresentsLaplace.laplaceTransformENN_eq {μ : MeasureTheory.Measure NNReal} {f : ℝ → ℝ} (h : RepresentsLaplace μ f) (t : NNReal) : laplaceTransformENN μ t = ENNReal.ofReal (f ↑t)

A representing measure's extended-real Laplace transform is obtained by applying ENNReal.ofReal to the represented function on ℝ≥0.

Open-half-line representation predicate

def TauCeti.RepresentsLaplaceOnIoi (μ : MeasureTheory.Measure NNReal) (f : ℝ → ℝ) : Prop

A positive measure on ℝ≥0 represents f by its Laplace transform on (0, ∞) if the exponential kernel p ↦ e^{-tp} is integrable against it for every t > 0 and the resulting transform agrees with f there.

The measure is not required to be finite: that is the whole point of the open-half-line statement, and the integrability clause is what takes over the role finiteness plays in TauCeti.RepresentsLaplace.

Equations

• TauCeti.RepresentsLaplaceOnIoi μ f = ((∀ (t : ℝ), 0 < t → MeasureTheory.Integrable (fun (p : NNReal) => Real.exp (-(t * ↑p))) μ) ∧ ∀ (t : ℝ), 0 < t → f t = TauCeti.laplaceTransform μ t)

theorem TauCeti.representsLaplaceOnIoi_iff {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} : RepresentsLaplaceOnIoi μ f ↔ (∀ (t : ℝ), 0 < t → MeasureTheory.Integrable (fun (p : NNReal) => Real.exp (-(t * ↑p))) μ) ∧ ∀ (t : ℝ), 0 < t → f t = laplaceTransform μ t

RepresentsLaplaceOnIoi μ f unfolds to integrability of the exponential kernel at every positive parameter together with equality with the Laplace transform there.

theorem TauCeti.RepresentsLaplaceOnIoi.integrable {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplaceOnIoi μ f) {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (p : NNReal) => Real.exp (-(t * ↑p))) μ

The exponential kernel is integrable against a representing measure at positive parameters.

theorem TauCeti.RepresentsLaplaceOnIoi.eq_laplaceTransform {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplaceOnIoi μ f) {t : ℝ} (ht : 0 < t) : f t = laplaceTransform μ t

A representing measure has the advertised Laplace-transform values on (0, ∞).

theorem TauCeti.RepresentsLaplaceOnIoi.sigmaFinite {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplaceOnIoi μ f) : MeasureTheory.SigmaFinite μ

A measure representing a function by its Laplace transform on (0, ∞) is sigma-finite.

theorem TauCeti.RepresentsLaplaceOnIoi.congr {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} {g : ℝ → ℝ} (hf : RepresentsLaplaceOnIoi μ f) (h : Set.EqOn g f (Set.Ioi 0)) : RepresentsLaplaceOnIoi μ g

A representation transports along agreement on the positive half-line: the predicate constrains f only there.

theorem TauCeti.RepresentsLaplaceOnIoi.add {f g : ℝ → ℝ} {μ ν : MeasureTheory.Measure NNReal} (hf : RepresentsLaplaceOnIoi μ f) (hg : RepresentsLaplaceOnIoi ν g) : RepresentsLaplaceOnIoi (μ + ν) (f + g)

The sum of two representing measures represents the sum of the functions on the positive half-line.

theorem TauCeti.RepresentsLaplaceOnIoi.smul {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (c : NNReal) (hf : RepresentsLaplaceOnIoi μ f) : RepresentsLaplaceOnIoi (↑c • μ) fun (t : ℝ) => ↑c * f t

Scaling a representing measure by c : ℝ≥0 represents the scaled function on the positive half-line.

theorem TauCeti.RepresentsLaplaceOnIoi.isCompletelyMonotoneOnIoi {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplaceOnIoi μ f) : IsCompletelyMonotoneOnIoi f

Easy direction: a represented function is completely monotone on (0, ∞).

theorem TauCeti.representsLaplaceOnIoi_zero : RepresentsLaplaceOnIoi 0 0

The zero measure represents the zero function on the positive half-line.

theorem TauCeti.RepresentsLaplace.representsLaplaceOnIoi {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplace μ f) : RepresentsLaplaceOnIoi μ f

A finite representing measure represents on the open half-line as well: the finiteness clause supplies the integrability clause, and (0, ∞) ⊆ [0, ∞).

theorem TauCeti.representsLaplace_zero : RepresentsLaplace 0 0

The zero measure represents the zero function.

theorem TauCeti.representsLaplace_dirac (x₀ : NNReal) : RepresentsLaplace (MeasureTheory.Measure.dirac x₀) fun (t : ℝ) => Real.exp (-(t * ↑x₀))

The Dirac mass at x₀ represents the exponential kernel t ↦ exp (-(t · x₀)).

Uniqueness: finite measures are determined by their Laplace transforms

theorem TauCeti.Measure.ext_of_forall_laplaceTransform_natCast_eq {μ ν : MeasureTheory.Measure NNReal} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (n : ℕ), laplaceTransform μ ↑n = laplaceTransform ν ↑n) : μ = ν

Finite measures on ℝ≥0 are determined by the values of their Laplace transforms at the natural numbers alone; this is the transform-level form of Measure.ext_of_forall_integral_exp_neg_natCast_mul_eq.

theorem TauCeti.RepresentsLaplace.unique {f : ℝ → ℝ} {μ ν : MeasureTheory.Measure NNReal} (hμ : RepresentsLaplace μ f) (hν : RepresentsLaplace ν f) : μ = ν

A function has at most one finite representing measure.