Completely Monotone

Results named in Tau Ceti's TauCeti.Analysis.CompletelyMonotone modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremBernstein's theorem, existence half#

A completely monotone function on [0, ∞) is the Laplace transform of a finite positive measure on ℝ≥0.

Uniqueness of that measure is not asserted here; it is TauCeti.RepresentsLaplace.unique, and the two combine in the Hausdorff--Bernstein--Widder theorem.

TauCeti.exists_representsLaplace_of_isCompletelyMonotone {f : ℝ → ℝ}
  (hcm : TauCeti.IsCompletelyMonotone f) : ∃ μ, TauCeti.RepresentsLaplace μ f

Lean

Formalized in Tau Ceti as TauCeti.exists_representsLaplace_of_isCompletelyMonotone.

Sources

• Tau Ceti documentation: TauCeti.exists_representsLaplace_of_isCompletelyMonotone
• Source of TauCeti.exists_representsLaplace_of_isCompletelyMonotone in TauCeti/Analysis/CompletelyMonotone/Bernstein/Theorem.lean

LeanTauCeti.exists_representsLaplace_of_isCompletelyMonotone

Uses 1 · Used by 2

Proof usesProkhorov's theorem for finite measures

Used byExistence half of the Hausdorff--Bernstein--Widder theorem · Hausdorff--Bernstein--Widder theorem, finite-measure version on ℝ≥0

TheoremThe complete Bernstein representation theorem, uniqueness form#

A complete Bernstein function has exactly one representing triple (a, b, μ).

TauCeti.IsCompleteBernsteinFunction.existsUnique_representsCompleteBernstein {f : ℝ → ℝ}
  (hf : TauCeti.IsCompleteBernsteinFunction f) :
  ∃! p, TauCeti.RepresentsCompleteBernstein p.2.2 p.1 p.2.1 f

Lean

Formalized in Tau Ceti as TauCeti.IsCompleteBernsteinFunction.existsUnique_representsCompleteBernstein.

Sources

• Tau Ceti documentation: TauCeti.IsCompleteBernsteinFunction.existsUnique_representsCompleteBernstein
• Source of TauCeti.IsCompleteBernsteinFunction.existsUnique_representsCompleteBernstein in TauCeti/Analysis/CompletelyMonotone/Stieltjes/Uniqueness.lean

LeanTauCeti.IsCompleteBernsteinFunction.existsUnique_representsCompleteBernstein

Uses 1

Proof usesMoment determinacy, exponential-moment form (the roadmap's B1 hypothesis)

TheoremThe Stieltjes representation theorem, uniqueness form#

A Stieltjes function has exactly one representing triple (a, b, μ).

TauCeti.IsStieltjesFunction.existsUnique_representsStieltjes {f : ℝ → ℝ}
  (hf : TauCeti.IsStieltjesFunction f) : ∃! p, TauCeti.RepresentsStieltjes p.2.2 p.1 p.2.1 f

Lean

Formalized in Tau Ceti as TauCeti.IsStieltjesFunction.existsUnique_representsStieltjes.

Sources

• Tau Ceti documentation: TauCeti.IsStieltjesFunction.existsUnique_representsStieltjes
• Source of TauCeti.IsStieltjesFunction.existsUnique_representsStieltjes in TauCeti/Analysis/CompletelyMonotone/Stieltjes/Uniqueness.lean

LeanTauCeti.IsStieltjesFunction.existsUnique_representsStieltjes

Uses 1

Proof usesMoment determinacy, exponential-moment form (the roadmap's B1 hypothesis)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.