Documentation

TauCeti.Analysis.CompletelyMonotone.FiniteDifference.Laplace

The Hausdorff--Bernstein--Widder theorem in finite-difference form #

Bernstein's theorem in the form TauCeti.exists_representsLaplace_of_isCompletelyMonotone takes a completely monotone function, that is a smooth one with alternating iterated derivatives, and produces a finite measure on ℝ≥0 whose Laplace transform it is. The hypothesis available in applications is the finite-difference one of TauCeti.IsDifferenceCompletelyMonotone, which carries no smoothness: what one can check about the mass of a family of measures, or about a function built from positive-definiteness data, is that its mixed forward differences alternate in sign.

This file closes the gap between the two, in both directions.

Feeding the smoothing of TauCeti.IsDifferenceCompletelyMonotone.exists_isCompletelyMonotone_between_shift into Bernstein's theorem bridges them up to an arbitrarily small shift of the argument: a function on [0, ∞) all of whose mixed forward differences alternate is squeezed, for every ε > 0, between the shift f (· + ε) and f by the Laplace transform of a finite measure (TauCeti.IsDifferenceCompletelyMonotone.exists_isFiniteMeasure_laplaceTransform_between_shift).

Compactness alone does not remove the shift, because the finite-difference hypothesis says nothing about the behaviour of f at the endpoint: the indicator f 0 = 1, f t = 0 for t ≠ 0 has every mixed difference with nonnegative steps of the required sign on [0, ∞) — with all steps positive, the only surviving term of Δ_{h₁} ⋯ Δ_{hₙ} f at a point of [0, ∞) is (-1)ⁿ f 0 at the origin — while no finite positive measure has it as its Laplace transform. Right-continuity at 0 is enough: it makes the Laplace gaps uniformly small, so Prokhorov gives a weak cluster point. The squeeze is closed at 0 by the assumed right-continuity and at positive parameters by continuity of the cluster point's Laplace transform.

For the converse, positive shifts of a continuous completely monotone function satisfy the finite-difference condition by the smooth equivalence in FiniteDifference/Basic.lean; closure under pointwise limits removes the shift. Applying this to a finite measure's Laplace transform gives the easy direction.

Together the two directions say that the finite-difference notion plus right-continuity at zero is equivalent to the derivative notion of TauCeti.IsContinuousCompletelyMonotoneOnIoi — no smoothness needs to be assumed, only concluded. TauCeti.IsDifferenceCompletelyMonotone.isContinuousCompletelyMonotoneOnIoi is the form in which applications use it: TauCeti.bernsteinMeasureKernel takes the derivative predicate as a hypothesis, and the representation API for TauCeti.bernsteinMeasure uses it.

Main declarations #

References #

Approximate representation from the finite-difference hypothesis #

source
theorem TauCeti.IsDifferenceCompletelyMonotone.exists_isFiniteMeasure_laplaceTransform_between_shift {f : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) {ε : ℝ} (hε : 0 < ε) :
∃ (μ : MeasureTheory.Measure NNReal), MeasureTheory.IsFiniteMeasure μ ∧ ∀ (t : ℝ), 0 ≤ t → f (t + ε) ≤ laplaceTransform μ t ∧ laplaceTransform μ t ≤ f t

Approximate Bernstein representation. A function that is completely monotone in the finite-difference sense is squeezed, for every ε > 0, between f (· + ε) and f by the Laplace transform of a finite positive measure on ℝ≥0.

A Bernstein representation of f itself does not follow from these measures by compactness alone: the hypothesis leaves the value at the endpoint free, so it needs right-continuity of f at 0, which is what TauCeti.exists_representsLaplace_of_isDifferenceCompletelyMonotone_of_continuousWithinAt adds.

The easy direction: Laplace transforms have alternating mixed differences #

source
theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.isDifferenceCompletelyMonotone {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) :
IsDifferenceCompletelyMonotone f

A function continuous on [0, ∞) and completely monotone on (0, ∞) is completely monotone in the finite-difference sense. Positive shifts are smooth completely monotone functions, and the finite-difference predicate passes to their pointwise limit.

source
theorem TauCeti.isDifferenceCompletelyMonotone_laplaceTransform (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] :
IsDifferenceCompletelyMonotone (laplaceTransform μ)

The Laplace transform of a finite measure is completely monotone in the finite-difference sense. Every mixed forward difference with nonnegative steps has the sign (-1)ⁿ, because it is (-1)ⁿ times the integral of a nonnegative function.

source
theorem TauCeti.RepresentsLaplace.isDifferenceCompletelyMonotone {f : ℝ → ℝ} {μ : MeasureTheory.Measure NNReal} (h : RepresentsLaplace μ f) :
IsDifferenceCompletelyMonotone f

A function represented by a finite measure through its Laplace transform is completely monotone in the finite-difference sense.

Tightness of the approximating measures #

The representation theorem #

source
theorem TauCeti.exists_representsLaplace_of_isDifferenceCompletelyMonotone_of_continuousWithinAt {f : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) (hcont : ContinuousWithinAt f (Set.Ici 0) 0) :
∃ (μ : MeasureTheory.Measure NNReal), RepresentsLaplace μ f

The existence half of the Hausdorff--Bernstein--Widder theorem in finite-difference form. A function right-continuous at zero all of whose mixed forward differences with nonnegative steps have the sign (-1)ⁿ is the Laplace transform of a finite positive measure on ℝ≥0.

source
theorem TauCeti.hausdorff_bernstein_widder_difference (f : ℝ → ℝ) :
IsDifferenceCompletelyMonotone f ∧ ContinuousWithinAt f (Set.Ici 0) 0 ↔ ∃ (μ : MeasureTheory.Measure NNReal), RepresentsLaplace μ f

The Hausdorff--Bernstein--Widder theorem in finite-difference form. A function has alternating mixed forward differences and is right-continuous at zero if and only if it is the Laplace transform of a finite positive measure on ℝ≥0.

Compare TauCeti.hausdorff_bernstein_widder, which states the same representation equivalence using the derivative-based complete-monotonicity hypothesis.

source
theorem TauCeti.hausdorff_bernstein_widder_difference_existsUnique (f : ℝ → ℝ) :
IsDifferenceCompletelyMonotone f ∧ ContinuousWithinAt f (Set.Ici 0) 0 ↔ ∃! μ : MeasureTheory.Measure NNReal, RepresentsLaplace μ f

Unique-existence form of the Hausdorff--Bernstein--Widder theorem in finite-difference form.

source
theorem TauCeti.isContinuousCompletelyMonotoneOnIoi_iff_isDifferenceCompletelyMonotone_and_continuousWithinAt (f : ℝ → ℝ) :
IsContinuousCompletelyMonotoneOnIoi f ↔ IsDifferenceCompletelyMonotone f ∧ ContinuousWithinAt f (Set.Ici 0) 0

The two notions of complete monotonicity agree under endpoint continuity. Complete monotonicity in the derivative sense on (0, ∞), together with continuity on [0, ∞), is equivalent to the sign condition on all mixed forward differences plus right-continuity at zero. Compare TauCeti.isCompletelyMonotone_iff_isDifferenceCompletelyMonotone, which assumes smoothness; here smoothness is a conclusion.

source
theorem TauCeti.IsDifferenceCompletelyMonotone.isContinuousCompletelyMonotoneOnIoi {f : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) (hcont : ContinuousWithinAt f (Set.Ici 0) 0) :
IsContinuousCompletelyMonotoneOnIoi f

From finite differences to derivatives. This is the form in which applications use the equivalence: TauCeti.bernsteinMeasureKernel takes TauCeti.IsContinuousCompletelyMonotoneOnIoi as a hypothesis, and the representation lemmas TauCeti.representsLaplace_bernsteinMeasure and TauCeti.laplaceTransform_bernsteinMeasure use it for TauCeti.bernsteinMeasure, while what is checkable in practice is the finite-difference condition.