Real boundary values and the support of a Nevanlinna measure

A Nevanlinna representation

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

of a Pick function has imaginary part

Im F (u + i v) = b v + ∫ x, v (1 + x ^ 2) / |x - (u + i v)| ^ 2 ∂rho(x),

a Poisson integral against the weighted measure (1 + x ^ 2) rho(dx). Where the boundary values of F are real, that Poisson integral must die as v tends to 0, and rho can carry no mass there: this is the vanishing half of the Stieltjes--Perron inversion formula.

The argument here is elementary. On the interval [u - v, u + v] the Poisson kernel is at least 1 / (2 v), so rho [u - v, u + v] ≤ 2 v * Im F (u + i v); covering a compact interval by N such intervals of half-width v = (b - a) / (2 N), on which Im F (· + i v) is uniformly small, bounds rho [a, b] by an arbitrarily small multiple of b - a.

One consequence recorded here is the one the theory of complete Bernstein functions needs: a Pick function that continues holomorphically across the positive half-axis and is real there has a Nevanlinna representation whose measure lives on (-∞, 0]. For a measure with this support, the kernel integral is continuous at positive real parameters, and an upper-half-plane representation extends to such a parameter when the function is continuous there from within the upper half-plane.

Main declarations

• TauCeti.measureReal_Icc_le_of_eq_nevanlinnaKernel_add: the Poisson lower bound rho [u - v, u + v] ≤ 2 v * Im F (u + i v).
• TauCeti.measure_Icc_eq_zero_of_eq_nevanlinnaKernel_add: a Nevanlinna measure gives no mass to a compact interval across which its imaginary part is continuous and has zero boundary values.
• TauCeti.exists_isFiniteMeasure_eq_nevanlinnaKernel_add_of_im_eq_zero: a Pick function that is holomorphic on the slit plane and real on (0, ∞) has a Nevanlinna measure vanishing on (0, ∞).
• TauCeti.continuousAt_integral_nevanlinnaKernel_of_measure_Ioi_eq_zero: continuity of the kernel integral at a point with positive real part for a measure supported on (-∞, 0].
• TauCeti.eq_integral_nevanlinnaKernel_add_of_eqOn_upperHalfPlane: extension of the representation to a positive real parameter.

References

• N. I. Akhiezer, The Classical Moment Problem and Some Related Questions in Analysis, Section 3.1 (the Stieltjes--Perron inversion formula).
• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, 2nd ed., Chapter 6.

theorem TauCeti.measureReal_Icc_le_of_eq_nevanlinnaKernel_add {F : ℂ → ℂ} {mu : MeasureTheory.Measure ℝ} {beta c : ℝ} [MeasureTheory.IsFiniteMeasure mu] (hbeta : 0 ≤ beta) (hrep : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, F z = ↑beta * z + ∫ (x : ℝ), nevanlinnaKernel z x ∂mu + ↑c) (u : ℝ) {v : ℝ} (hv : 0 < v) : mu.real (Set.Icc (u - v) (u + v)) ≤ 2 * v * (F (↑u + ↑v * Complex.I)).im

The Poisson lower bound of a Nevanlinna representation. The mass a Nevanlinna measure gives to the interval of centre u and half-width v is at most 2 v times the imaginary part of the represented function at u + i v.

theorem TauCeti.measure_Icc_eq_zero_of_eq_nevanlinnaKernel_add {F : ℂ → ℂ} {mu : MeasureTheory.Measure ℝ} {beta c : ℝ} [MeasureTheory.IsFiniteMeasure mu] (hrep : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, F z = ↑beta * z + ∫ (x : ℝ), nevanlinnaKernel z x ∂mu + ↑c) {a b d : ℝ} (hab : a < b) (hd : 0 < d) (hcont : ContinuousOn (fun (z : ℂ) => (F z).im) (Set.Icc a b ×ℂ Set.Icc 0 d)) (hzero : ∀ u ∈ Set.Icc a b, (F ↑u).im = 0) : mu (Set.Icc a b) = 0

The Stieltjes--Perron vanishing theorem. A Nevanlinna measure gives no mass to a compact interval over which the imaginary part of the represented function is continuous up to the real axis and vanishes there. Continuity is asked for on the closed rectangle of any positive height d over the interval, as a function holomorphic near the interval supplies it.

theorem TauCeti.continuousAt_integral_nevanlinnaKernel_of_measure_Ioi_eq_zero {rho : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure rho] (hrho : rho (Set.Ioi 0) = 0) {z₀ : ℂ} (hz₀ : 0 < z₀.re) : ContinuousAt (fun (z : ℂ) => ∫ (x : ℝ), nevanlinnaKernel z x ∂rho) z₀

The Nevanlinna integral of a finite measure carried by (-∞, 0] is continuous at every point with positive real part. Although the kernel has a pole on the real axis, that pole stays a positive distance from the measure's support.

theorem TauCeti.eq_integral_nevanlinnaKernel_add_of_eqOn_upperHalfPlane {F : ℂ → ℂ} {rho : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure rho] {b c t : ℝ} (hF : ContinuousWithinAt F UpperHalfPlane.upperHalfPlaneSet ↑t) (hrho : rho (Set.Ioi 0) = 0) (ht : 0 < t) (hrep : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, F z = ↑b * z + ∫ (x : ℝ), nevanlinnaKernel z x ∂rho + ↑c) : F ↑t = ↑b * ↑t + ∫ (x : ℝ), nevanlinnaKernel (↑t) x ∂rho + ↑c

A Nevanlinna representation valid on the upper half-plane holds at a positive real parameter t at which F is continuous from within the upper half-plane, provided its measure is carried by (-∞, 0].

theorem TauCeti.exists_isFiniteMeasure_eq_nevanlinnaKernel_add_of_im_eq_zero {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F Complex.slitPlane) (him : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, 0 ≤ (F z).im) (hzero : ∀ (t : ℝ), 0 < t → (F ↑t).im = 0) : ∃ (rho : MeasureTheory.Measure ℝ) (b : ℝ), MeasureTheory.IsFiniteMeasure rho ∧ 0 ≤ b ∧ rho (Set.Ioi 0) = 0 ∧ ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, F z = ↑b * z + ∫ (x : ℝ), nevanlinnaKernel z x ∂rho + ↑(F Complex.I).re

The Nevanlinna measure of a Pick function real on the positive half-axis. A function that is holomorphic on the slit plane, has nonnegative imaginary part on the upper half-plane and is real on (0, ∞) admits a Nevanlinna representation whose measure vanishes on (0, ∞).