Uniqueness of the Stieltjes and complete Bernstein representations

A Stieltjes function determines the data representing it: if

f t = a / t + b + ∫ (t + x)⁻¹ dμ(x) for all t > 0

with a, b ≥ 0 and μ a measure on ℝ≥0 without an atom at the origin whose standard weight x ↦ (1 + x)⁻¹ is integrable, then a, b and μ are uniquely determined by f. This is the uniqueness half of the Stieltjes representation, and it transfers verbatim to complete Bernstein functions through TauCeti.RepresentsCompleteBernstein.representsStieltjes_div.

The three pieces of data are separated one at a time.

• The coefficient b is the limit of f at +∞, because the Stieltjes integral vanishes there (TauCeti.tendsto_integral_inv_add_atTop_nhds_zero) and so does a / t.
• The singular coefficient a is the mass that the measure a • δ₀ + μ puts at the origin, since a / t is exactly the Stieltjes integral of a • δ₀. So once b is known, the whole representation is the Stieltjes transform of a single measure, and it remains to show that a measure is determined by its Stieltjes transform.
• That determinacy (TauCeti.Measure.ext_of_integral_inv_add_eventuallyEq) reduces to Laplace determinacy for finite measures. Differentiating the Stieltjes transform n times at t = 1 (TauCeti.iteratedDeriv_integral_inv_add) recovers the numbers ∫ (1 + x)^{-1-n} dμ, which are the values at the natural numbers of the Laplace transform of the finite measure obtained by weighting μ with (1 + x)⁻¹ and pushing it forward along x ↦ log (1 + x). A finite measure on ℝ≥0 is determined by those values (TauCeti.Measure.ext_of_forall_laplaceTransform_natCast_eq), and both the pushforward and the weighting are invertible.

Main declarations

• TauCeti.tendsto_integral_inv_add_atTop_nhds_zero: a Stieltjes transform vanishes at +∞.
• TauCeti.Measure.ext_of_integral_inv_add_eventuallyEq: a measure on ℝ≥0 with integrable Stieltjes weight is determined by the germ of its Stieltjes transform at 1.
• TauCeti.RepresentsStieltjes.unique and TauCeti.IsStieltjesFunction.existsUnique_representsStieltjes: uniqueness of the Stieltjes representation.
• TauCeti.RepresentsCompleteBernstein.unique and TauCeti.IsCompleteBernsteinFunction.existsUnique_representsCompleteBernstein: uniqueness of the complete Bernstein representation.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, de Gruyter, 2nd ed. (2012), Theorem 2.2 and Theorem 6.2.

The Stieltjes transform at infinity

theorem TauCeti.tendsto_integral_inv_add_atTop_nhds_zero {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : NNReal), (t + ↑x)⁻¹ ∂μ) Filter.atTop (nhds 0)

A Stieltjes transform vanishes at infinity. The integrand (t + x)⁻¹ is dominated by the standard Stieltjes weight once t ≥ 1, and tends to 0 pointwise.

Determinacy of a measure by its Stieltjes transform

The Stieltjes weight is turned into an exponential by the substitution y = log (1 + x), whose inverse is x = exp y - 1; both are recorded as self-maps of ℝ≥0, so that the transported measure is again a measure on ℝ≥0.

theorem TauCeti.Measure.ext_of_integral_inv_add_eventuallyEq {μ ν : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hν : MeasureTheory.Integrable stieltjesWeight ν) (h : (fun (t : ℝ) => ∫ (x : NNReal), (t + ↑x)⁻¹ ∂μ) =ᶠ[nhds 1] fun (t : ℝ) => ∫ (x : NNReal), (t + ↑x)⁻¹ ∂ν) : μ = ν

A measure on ℝ≥0 whose Stieltjes weight is integrable is determined by the germ of its Stieltjes transform at 1.

Uniqueness of the representing data

The singular coefficient is absorbed into the representing measure as an atom at the origin, which turns a Stieltjes representation into an additive constant plus a single Stieltjes transform.

theorem TauCeti.RepresentsStieltjes.unique {μ ν : MeasureTheory.Measure NNReal} {a b c d : NNReal} {f : ℝ → ℝ} (hf : RepresentsStieltjes μ a b f) (hg : RepresentsStieltjes ν c d f) : a = c ∧ b = d ∧ μ = ν

Uniqueness of the Stieltjes representation. A Stieltjes function determines its singular coefficient, its additive constant, and its representing measure.

theorem TauCeti.RepresentsCompleteBernstein.unique {μ ν : MeasureTheory.Measure NNReal} {a b c d : NNReal} {f : ℝ → ℝ} (hf : RepresentsCompleteBernstein μ a b f) (hg : RepresentsCompleteBernstein ν c d f) : a = c ∧ b = d ∧ μ = ν

Uniqueness of the complete Bernstein representation. A complete Bernstein function determines its two coefficients and its representing measure, because dividing by the parameter turns it into a Stieltjes function with the same data.

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

The Stieltjes representation theorem, uniqueness form. A Stieltjes function has exactly one representing triple (a, b, μ).

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

The complete Bernstein representation theorem, uniqueness form. A complete Bernstein function has exactly one representing triple (a, b, μ).