Pick functions in Cayley coordinates

A Pick function is holomorphic on the upper half-plane and has nonnegative imaginary part there. The Cayley coordinate z ↦ (z - i) / (z + i) carries the upper half-plane to the unit disc, and multiplication by -i carries nonnegative imaginary part to nonnegative real part. The Herglotz representation on the disc therefore gives

F z = i · ∫ ζ, (ζ + w) / (ζ - w) ∂μ(ζ) + Re F(i),

where w = (z - i) / (z + i) and μ is a finite positive measure on the unit circle. The converse holds as well. This is the Cayley-coordinate form of the Pick representation; moving the circle measure to the real line gives the usual Nevanlinna representation.

Main declarations

• TauCeti.exists_isFiniteMeasure_eq_I_mul_herglotzTransform_cayley_add: existence of the Cayley-coordinate Herglotz representation of a Pick function.
• TauCeti.differentiableOn_and_im_nonneg_iff_exists_eq_I_mul_herglotzTransform_cayley_add: the characterization of Pick functions by this representation.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, 2nd ed., Chapter 6.

theorem TauCeti.exists_isFiniteMeasure_eq_I_mul_herglotzTransform_cayley_add {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F UpperHalfPlane.upperHalfPlaneSet) (him : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, 0 ≤ (F z).im) : ∃ (μ : MeasureTheory.Measure Circle), MeasureTheory.IsFiniteMeasure μ ∧ ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, F z = Complex.I * μ.herglotzTransform ((z - Complex.I) / (z + Complex.I)) + ↑(F Complex.I).re

Cayley-coordinate Herglotz representation of a Pick function. A function holomorphic on the upper half-plane with nonnegative imaginary part is, after the Cayley coordinate z ↦ (z - i) / (z + i), i times the Herglotz transform of a finite positive measure on the unit circle, plus the real constant Re F(i).

theorem TauCeti.differentiableOn_and_im_nonneg_iff_exists_eq_I_mul_herglotzTransform_cayley_add {F : ℂ → ℂ} : (DifferentiableOn ℂ F UpperHalfPlane.upperHalfPlaneSet ∧ ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, 0 ≤ (F z).im) ↔ ∃ (μ : MeasureTheory.Measure Circle) (a : ℝ), MeasureTheory.IsFiniteMeasure μ ∧ ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, F z = Complex.I * μ.herglotzTransform ((z - Complex.I) / (z + Complex.I)) + ↑a

Characterization of Pick functions in Cayley coordinates. A function is holomorphic on the upper half-plane with nonnegative imaginary part if and only if it is i times the Herglotz transform of a finite positive circle measure in the Cayley coordinate, plus a real constant.