The Herglotz representation of holomorphic functions with nonnegative real part

A function F holomorphic on the unit disc with 0 ≤ re F is the Herglotz transform of a finite positive measure μ on the unit circle, up to an imaginary constant:

F w = ∫ (z + w) / (z - w) dμ(z) + (im F(0)) i,

and conversely every such transform is holomorphic on the disc with nonnegative real part. The representation is the basic structure theorem for holomorphic functions of positive real part (Carathéodory functions). Through a Cayley transform it gives the Nevanlinna representation of Pick functions, which in turn underlies the analytic characterizations of Stieltjes and complete Bernstein functions.

Main results

• DiffContOnCl.circleAverage_herglotzRieszKernel_smul_re_add: the Herglotz formula on a disc, recovering a holomorphic function from the boundary values of its real part.
• MeasureTheory.Measure.herglotzTransform: the Herglotz transform of a measure on the circle.
• MeasureTheory.Measure.differentiableOn_herglotzTransform and MeasureTheory.Measure.re_herglotzTransform_nonneg: the transform of a finite measure is holomorphic on the disc with nonnegative real part.
• TauCeti.exists_isFiniteMeasure_eq_herglotzTransform_add: the Herglotz representation theorem.
• TauCeti.differentiableOn_and_re_nonneg_iff_exists_eq_herglotzTransform_add: the resulting characterization of holomorphic functions on the disc with nonnegative real part.

References

• G. Herglotz, Über Potenzreihen mit positivem, reellem Teil im Einheitskreis, Ber. Verh. Sächs. Akad. Wiss. Leipzig 63 (1911), 501–511.
• W. Rudin, Real and Complex Analysis, 3rd ed., Chapter 11 (positive harmonic functions and the Herglotz representation).
• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, 2nd ed., Chapter 6 (the Nevanlinna–Pick representation, via the Herglotz theorem).

theorem DiffContOnCl.circleAverage_herglotzRieszKernel_smul_re_add {f : ℂ → ℂ} {c w : ℂ} {R : ℝ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hw : w ∈ Metric.ball c R) : Real.circleAverage (fun (ζ : ℂ) => herglotzRieszKernel c w ζ • ↑(f ζ).re) c R + ↑(f c).im * Complex.I = f w

The Herglotz formula on a disc: a function holomorphic on a disc and continuous up to its boundary is the Herglotz–Riesz integral of its boundary real part, plus the imaginary constant (f c).im * I. Unlike the Poisson formula, which recovers f from all of its boundary values, this recovers f from the boundary values of its real part alone.

The Herglotz transform of a measure on the circle

noncomputable def MeasureTheory.Measure.herglotzTransform (μ : Measure Circle) (w : ℂ) : ℂ

The Herglotz transform of a measure on the unit circle.

Equations

• μ.herglotzTransform w = ∫ (z : Circle), (↑z + w) / (↑z - w) ∂μ

theorem MeasureTheory.Measure.herglotzTransform_def (μ : Measure Circle) (w : ℂ) : μ.herglotzTransform w = ∫ (z : Circle), (↑z + w) / (↑z - w) ∂μ

The Herglotz transform written as its defining integral.

@[simp]

theorem MeasureTheory.Measure.herglotzTransform_zero (μ : Measure Circle) : μ.herglotzTransform 0 = ↑(μ.real Set.univ)

The value at zero of the Herglotz transform is μ.real univ. For a finite measure this is its total mass; for an infinite measure both sides are 0, since μ.real univ = 0 and the Bochner integral of the non-integrable constant 1 is 0 by convention.

theorem MeasureTheory.Measure.differentiableOn_herglotzTransform (μ : Measure Circle) [IsFiniteMeasure μ] : DifferentiableOn ℂ μ.herglotzTransform (Metric.ball 0 1)

The Herglotz transform w ↦ ∫ (z + w) / (z - w) dμ(z) of a finite measure on the unit circle is holomorphic on the unit disc.

theorem MeasureTheory.Measure.re_herglotzTransform_nonneg {w : ℂ} (μ : Measure Circle) (hw : w ∈ Metric.ball 0 1) : 0 ≤ (μ.herglotzTransform w).re

The Herglotz transform of a measure on the unit circle has nonnegative real part on the unit disc.

The Herglotz representation

theorem TauCeti.exists_isFiniteMeasure_eq_herglotzTransform_add {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F (Metric.ball 0 1)) (hre : ∀ w ∈ Metric.ball 0 1, 0 ≤ (F w).re) : ∃ (μ : MeasureTheory.Measure Circle), MeasureTheory.IsFiniteMeasure μ ∧ ∀ w ∈ Metric.ball 0 1, F w = μ.herglotzTransform w + ↑(F 0).im * Complex.I

The Herglotz representation theorem. A function holomorphic on the unit disc with nonnegative real part is the Herglotz transform ∫ (z + w) / (z - w) dμ(z) of a finite positive measure μ on the unit circle, plus the imaginary constant (F 0).im * I.

theorem TauCeti.differentiableOn_and_re_nonneg_iff_exists_eq_herglotzTransform_add {F : ℂ → ℂ} : (DifferentiableOn ℂ F (Metric.ball 0 1) ∧ ∀ w ∈ Metric.ball 0 1, 0 ≤ (F w).re) ↔ ∃ (μ : MeasureTheory.Measure Circle) (b : ℝ), MeasureTheory.IsFiniteMeasure μ ∧ ∀ w ∈ Metric.ball 0 1, F w = μ.herglotzTransform w + ↑b * Complex.I

The Herglotz representation theorem, as a characterization: a function on the unit disc is holomorphic with nonnegative real part if and only if it is the Herglotz transform of a finite positive measure on the unit circle plus an imaginary constant.