Complete Bernstein functions from a Nevanlinna representation off the positive half-axis

A Nevanlinna representation

F(z) = c + b z + ∫ x, (1 + x z) / (x - z) ∂ρ

with a finite measure ρ carried by (-∞, 0] restricts on (0, ∞) to a real function, and this file converts such data into complete-Bernstein representing data whenever that restriction is nonnegative.

Reflecting ρ to the finite measure ν on ℝ≥0 obtained by pushing forward along x ↦ -x, the kernel becomes (t y - 1) / (t + y) = t - (1 + t ^ 2) / (t + y), so the representation reads

f(t) = c + (b + ν(ℝ≥0)) t - (1 + t ^ 2) ∫ y, (t + y)⁻¹ ∂ν.

Nonnegativity of f on (0, ∞) bounds the Stieltjes transform ∫ y, (t + y)⁻¹ ∂ν by an affine function of t, and letting t decrease to zero turns that bound into the finiteness of ∫ y, y⁻¹ ∂ν, the pivot of the whole argument: it forbids an atom of ν at 0, it makes the weighted measure μ = (1 + y ^ 2) y⁻¹ ν satisfy the Stieltjes weight condition, and it makes the constant c - ∫ y, y⁻¹ ∂ν nonnegative. The pointwise identity

(1 + y ^ 2) y⁻¹ · t / (t + y) = y⁻¹ + t - (1 + t ^ 2) / (t + y) (y > 0)

then rewrites the representation as f(t) = (c - ∫ y, y⁻¹ ∂ν) + b t + ∫ y, t / (t + y) ∂μ, which is the complete-Bernstein form.

This is the half of the analytic characterization of complete Bernstein functions that starts from the Nevanlinna data; the converse, that a complete Bernstein function extends to a Pick function on the slit plane, is TauCeti.IsCompleteBernsteinFunction.exists_analyticOnNhd_slitPlane.

Main declarations

• TauCeti.exists_isCompleteBernsteinFunction_eqOn_of_eq_integral_reflected_nevanlinnaKernel: the reflected form of the conversion, for a measure on ℝ≥0.
• TauCeti.exists_isCompleteBernsteinFunction_eqOn_of_eq_integral_nevanlinnaKernel: the conversion, for Nevanlinna data on ℝ carried by (-∞, 0].

References

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

theorem TauCeti.exists_isCompleteBernsteinFunction_eqOn_of_eq_integral_reflected_nevanlinnaKernel {ν : MeasureTheory.Measure NNReal} [MeasureTheory.IsFiniteMeasure ν] {b c : ℝ} (hb : 0 ≤ b) {f : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 < t → f t = c + b * t + ∫ (y : NNReal), (t * ↑y - 1) / (t + ↑y) ∂ν) (hpos : ∀ (t : ℝ), 0 < t → 0 ≤ f t) : ∃ (g : ℝ → ℝ), IsCompleteBernsteinFunction g ∧ Set.EqOn g f (Set.Ioi 0)

Complete Bernstein functions from reflected Nevanlinna data. A function that agrees on (0, ∞) with c + b t + ∫ y, (t y - 1) / (t + y) ∂ν, for a finite measure ν on ℝ≥0 and b ≥ 0, and is nonnegative there, agrees on (0, ∞) with a complete Bernstein function.

The integrand is the Nevanlinna kernel (1 + x t) / (x - t) after the reflection x = -y that carries (-∞, 0] onto ℝ≥0.

theorem TauCeti.exists_isCompleteBernsteinFunction_eqOn_of_eq_integral_nevanlinnaKernel {ρ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure ρ] (hρ : ρ (Set.Ioi 0) = 0) {b c : ℝ} (hb : 0 ≤ b) {f : ℝ → ℝ} (hf : ∀ (t : ℝ), 0 < t → ↑(f t) = ↑b * ↑t + ∫ (x : ℝ), nevanlinnaKernel (↑t) x ∂ρ + ↑c) (hpos : ∀ (t : ℝ), 0 < t → 0 ≤ f t) : ∃ (g : ℝ → ℝ), IsCompleteBernsteinFunction g ∧ Set.EqOn g f (Set.Ioi 0)

Complete Bernstein functions from a Nevanlinna representation off the positive half-axis. A function that agrees on (0, ∞) with the Nevanlinna transform `b t + ∫ x, (1 + x t) / (x - t) ∂ρ

• cof a nonnegative coefficientband a finite measureρgiving no mass to(0, ∞), and is nonnegative there, agrees on (0, ∞)` with a complete Bernstein function.