A finite measure on ℝ≥0 is determined by its Laplace transform #
Main results #
TauCeti.Measure.ext_of_forall_integral_exp_neg_natCast_mul_eq— the sharp form: the transform's values at the natural numbers already determine the measure.TauCeti.Measure.ext_of_forall_integral_exp_neg_mul_eq— the convenience form, hypothesis at every nonnegative real.
Implementation #
The substitution y = e^{-x} converts the Laplace transform into a moment sequence: at a natural
argument n, ∫ e^{-n x} dμ = ∫ yⁿ d(μ.map (x ↦ e^{-x})). So matching Laplace transforms give
pushforwards with matching moments, and the pushforwards are moment-determinate because they are
carried by (0, 1] — bounded support makes the exponential-moment hypothesis of
Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp automatic. Finally x ↦ e^{-x} is
injective and measurable between standard Borel spaces, hence a measurable embedding by
Lusin–Souslin, and MeasurableEmbedding.map_injective recovers μ = ν from the equal pushforwards.
Only the transform's values at natural arguments are used, which is why the primary statement
quantifies over ℕ; the real-argument form is a one-line corollary for callers that have it.
This is the uniqueness half of the Bernstein milestone in
TauCetiRoadmap/OneParameterSemigroups/README.md, Part B. The existence half is a separate,
independent development, and the two are combined in the Hausdorff--Bernstein--Widder theorem
(TauCeti.hausdorff_bernstein_widder_existsUnique in
Analysis/CompletelyMonotone/Bernstein/HausdorffBernsteinWidder.lean).
Nothing here mentions complete monotonicity — the statement is about two arbitrary
finite measures — which is why it lives beside the other determinacy results rather than under
Analysis/CompletelyMonotone/.
A finite measure on ℝ≥0 is determined by its Laplace transform at the natural numbers.
Substituting y = e^{-x} turns the value at n into the n-th moment of the pushforward, which is
carried by (0, 1] and so is moment-determinate.
A finite measure on ℝ≥0 is determined by its Laplace transform. The convenience form
taking the hypothesis at every nonnegative real; the proof needs only the natural numbers, so
Measure.ext_of_forall_integral_exp_neg_natCast_mul_eq is the sharper statement.