Laplace uniqueness for finite measures on the nonnegative half-line

Two finite 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.finiteMeasure_eq_of_laplace_on_nonneg {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμ : μ (Set.Iio 0) = 0) (hν : ν (Set.Iio 0) = 0) (hL : ∀ (q : ℝ), 0 < q → ∫ (t : ℝ), Real.exp (-q * t) ∂μ = ∫ (t : ℝ), Real.exp (-q * t) ∂ν) : μ = ν

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

theorem BGW.StableTrees.measure_eq_withDensity_of_laplace {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ (Set.Iio 0) = 0) (hν : ν (Set.Iio 0) = 0) {f : ℝ → ℝ} (hf : Measurable f) (hi : MeasureTheory.Integrable f ν) (hL : ∀ (lam : ℝ), 0 < lam → ∫ (x : ℝ), Real.exp (-lam * x) ∂μ = ∫ (x : ℝ), Real.exp (-lam * x) * f x ∂ν) : (μ = ν.withDensity fun (x : ℝ) => ENNReal.ofReal (f x)) ∧ ∀ᵐ (x : ℝ) ∂ν, 0 ≤ f x

Signed integrable densities are identified before positivity: equality of their Laplace integrals with a finite nonnegative measure forces equality of measures and positivity almost everywhere on a nonnegative carrier.

theorem BGW.StableTrees.measure_eq_withDensity_of_laplace_halfline {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ (Set.Iio 0) = 0) (hν : ν (Set.Iio 0) = 0) {f : ℝ → ℝ} (hf : Measurable f) {a : ℝ} (ha : 0 < a) (hi : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-a * x) * f x) ν) (hL : ∀ (lam : ℝ), a < lam → ∫ (x : ℝ), Real.exp (-lam * x) ∂μ = ∫ (x : ℝ), Real.exp (-lam * x) * f x ∂ν) : (μ = ν.withDensity fun (x : ℝ) => ENNReal.ofReal (f x)) ∧ ∀ᵐ (x : ℝ) ∂ν, 0 ≤ f x

Laplace equality on a strict half-line identifies a signed density after exponential tilting. The sign conclusion concerns the real density before applying ENNReal.ofReal.