The Pick characterization of complete Bernstein functions

A function is complete Bernstein exactly when it is right-continuous at 0, nonnegative on (0, ∞), extends holomorphically to the slit plane ℂ \ (-∞, 0], and maps the upper half-plane into its closure. This is the analytic characterization of complete Bernstein functions.

The characterization is supported by boundary-continuity results for Nevanlinna representations, which transfer upper-half-plane formulas to positive real parameters. It therefore lets users recover complete-Bernstein representing data from a holomorphic Pick extension.

Main declarations

• TauCeti.exists_isCompleteBernsteinFunction_eqOn_of_analyticOnNhd: a nonnegative function with a Pick extension to the slit plane agrees on (0, ∞) with a complete Bernstein function.
• TauCeti.isCompleteBernsteinFunction_iff_continuousWithinAt_nonneg_exists_analyticOnNhd: the Pick characterization of complete Bernstein functions.

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_analyticOnNhd {f : ℝ → ℝ} {F : ℂ → ℂ} (hF : AnalyticOnNhd ℂ F Complex.slitPlane) (hFf : ∀ (t : ℝ), 0 < t → F ↑t = ↑(f t)) (him : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, 0 ≤ (F z).im) (hpos : ∀ (t : ℝ), 0 < t → 0 ≤ f t) : ∃ (g : ℝ → ℝ), IsCompleteBernsteinFunction g ∧ Set.EqOn g f (Set.Ioi 0)

Complete Bernstein functions from Pick extensions, on (0, ∞). A function that is nonnegative on (0, ∞) and has a holomorphic extension to the slit plane mapping the upper half-plane into its closure agrees on (0, ∞) with a complete Bernstein function. Unlike the characterization below, no condition at 0 is imposed.

theorem TauCeti.isCompleteBernsteinFunction_iff_continuousWithinAt_nonneg_exists_analyticOnNhd (f : ℝ → ℝ) : IsCompleteBernsteinFunction f ↔ ContinuousWithinAt f (Set.Ici 0) 0 ∧ (∀ (t : ℝ), 0 < t → 0 ≤ f t) ∧ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F Complex.slitPlane ∧ (∀ (t : ℝ), 0 < t → F ↑t = ↑(f t)) ∧ ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, 0 ≤ (F z).im

Pick characterization of complete Bernstein functions (Schilling--Song--Vondraček, Theorem 6.2). A real function is complete Bernstein exactly when it is right-continuous at 0, nonnegative on (0, ∞), and has a holomorphic extension to the slit plane that maps the upper half-plane into its closure.