Laplace uniqueness for laws on the nonnegative half-line

Two probability measures carried by [0, ∞) are equal when their Laplace transforms agree at all positive parameters. The proof uses analyticity in the left half-plane and dominated convergence at its imaginary boundary (W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971, Section XIII.1).

theorem BGW.StableTrees.measure_eq_of_laplace_on_nonneg {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : μ (Set.Iio 0) = 0) (hν : ν (Set.Iio 0) = 0) (hL : ∀ (q : ℝ), 0 < q → ∫ (t : ℝ), Real.exp (-q * t) ∂μ = ∫ (t : ℝ), Real.exp (-q * t) ∂ν) : μ = ν

Probability measures on [0, ∞) have equal laws if their Laplace transforms agree.