Reciprocals of Stieltjes and complete Bernstein functions

A function is Stieltjes exactly when its reciprocal agrees on (0, ∞) with a complete Bernstein function. Equivalently, if f is complete Bernstein then so is its conjugate f*(t) = t / f(t). This is the third correspondence between the two classes, alongside f ↦ t f(t) and f ↦ f(t⁻¹).

The proof is analytic. A complete Bernstein function f with data μ, a, b is t S(t) for the complex Stieltjes transform S of the same data, and S maps the upper half-plane into the closed lower half-plane. Unless the data vanish, S has no zero on the slit plane, so t / f(t) = S(t)⁻¹ extends holomorphically to the slit plane and maps the upper half-plane into its closure. The Pick characterization then produces the complete Bernstein function.

No nonvanishing hypothesis is needed: zero data represent the zero function, whose reciprocal and conjugate are again zero because 0⁻¹ = 0. So the statements here generalize the classical correspondence for nonzero functions to include the zero function, via Lean's convention 0⁻¹ = 0. Since t ↦ f(t)⁻¹ only sees f on (0, ∞), recovering that f itself is complete Bernstein also needs right-continuity at 0, which pins down f 0.

Main declarations

• TauCeti.IsCompleteBernsteinFunction.exists_isCompleteBernsteinFunction_eqOn_div: the conjugate t ↦ t / f(t) of a complete Bernstein function is complete Bernstein on (0, ∞).
• TauCeti.IsCompleteBernsteinFunction.isStieltjesFunction_inv: the reciprocal of a complete Bernstein function is Stieltjes.
• TauCeti.isStieltjesFunction_iff_exists_isCompleteBernsteinFunction_eqOn_inv: f is Stieltjes exactly when t ↦ f(t)⁻¹ on (0, ∞) extends to a complete Bernstein function.
• TauCeti.isCompleteBernsteinFunction_iff_continuousWithinAt_isStieltjesFunction_inv: f is complete Bernstein exactly when it is right-continuous at 0 and t ↦ f(t)⁻¹ is Stieltjes.

References

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

theorem TauCeti.IsCompleteBernsteinFunction.exists_isCompleteBernsteinFunction_eqOn_div {f : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) : ∃ (g : ℝ → ℝ), IsCompleteBernsteinFunction g ∧ Set.EqOn g (fun (t : ℝ) => t / f t) (Set.Ioi 0)

The conjugate of a complete Bernstein function (Schilling--Song--Vondraček, Chapter 7). If f is complete Bernstein, then t ↦ t / f(t) on (0, ∞) extends to a complete Bernstein function on [0, ∞).

theorem TauCeti.IsCompleteBernsteinFunction.isStieltjesFunction_inv {f : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) : IsStieltjesFunction fun (t : ℝ) => (f t)⁻¹

The reciprocal of a complete Bernstein function is Stieltjes.

theorem TauCeti.isStieltjesFunction_iff_exists_isCompleteBernsteinFunction_eqOn_inv {f : ℝ → ℝ} : IsStieltjesFunction f ↔ ∃ (g : ℝ → ℝ), IsCompleteBernsteinFunction g ∧ Set.EqOn g (fun (t : ℝ) => (f t)⁻¹) (Set.Ioi 0)

Stieltjes functions and complete Bernstein functions under reciprocals. A function f is Stieltjes exactly when t ↦ f(t)⁻¹ on (0, ∞) extends to a complete Bernstein function on [0, ∞).

theorem TauCeti.isCompleteBernsteinFunction_iff_continuousWithinAt_isStieltjesFunction_inv (f : ℝ → ℝ) : IsCompleteBernsteinFunction f ↔ ContinuousWithinAt f (Set.Ici 0) 0 ∧ IsStieltjesFunction fun (t : ℝ) => (f t)⁻¹

Complete Bernstein functions are the reciprocals of Stieltjes functions (Schilling--Song--Vondraček, Chapter 7). A function f is complete Bernstein exactly when it is right-continuous at 0 and t ↦ f(t)⁻¹ is Stieltjes. The continuity condition recovers f 0, which the reciprocal does not see; no nonvanishing hypothesis is needed, since for the zero function both sides hold.