The holomorphic extension of a Stieltjes function

A Stieltjes representation

f(t) = a / t + b + ∫ x, (t + x)⁻¹ ∂μ

makes sense for every complex z off the closed negative half-axis: on the slit plane ℂ ∖ (-∞, 0] the kernel (z + x)⁻¹ is dominated by a multiple of the Stieltjes weight (1 + x)⁻¹, locally uniformly in z. The resulting complex Stieltjes transform TauCeti.stieltjesExtension μ a b is holomorphic on the slit plane, restricts to f on (0, ∞), is symmetric under complex conjugation, and has imaginary part

Im F(z) = -Im z * (a / |z|² + ∫ x, |z + x|⁻² ∂μ),

so that Im z * Im F(z) ≤ 0: a Stieltjes function extends to a holomorphic function mapping the upper half-plane into the closed lower half-plane. Multiplying by z, a complete Bernstein function extends holomorphically to the slit plane with 0 ≤ Im z * Im G(z), i.e. to a Pick function. These are the forward halves of the analytic characterizations of Stieltjes and complete Bernstein functions. By the identity theorem, the extension is the only holomorphic function on the slit plane that agrees with f on (0, ∞).

Main declarations

• TauCeti.stieltjesExtension: the complex Stieltjes transform of representing data.
• TauCeti.integrable_inv_add_of_mem_slitPlane: the complex Stieltjes kernel is integrable at every point of the slit plane.
• TauCeti.hasDerivAt_stieltjesExtension and TauCeti.analyticOnNhd_stieltjesExtension: the transform is holomorphic on the slit plane, with derivative -a / z² - ∫ x, (z + x)⁻² ∂μ.
• TauCeti.stieltjesExtension_conj: the transform commutes with complex conjugation.
• TauCeti.stieltjesExtension_eq_zero_iff: the transform vanishes somewhere on the slit plane only when its data is zero.
• TauCeti.im_stieltjesExtension and TauCeti.im_mul_im_stieltjesExtension_nonpos: the imaginary part and its sign; TauCeti.im_mul_stieltjesExtension and TauCeti.im_mul_im_mul_stieltjesExtension_nonneg do the same for z ↦ z F(z).
• TauCeti.RepresentsStieltjes.stieltjesExtension_ofReal and TauCeti.RepresentsStieltjes.eqOn_stieltjesExtension: the transform extends the represented function, and is its only holomorphic extension to the slit plane.
• TauCeti.IsStieltjesFunction.exists_analyticOnNhd_slitPlane: a Stieltjes function extends holomorphically to the slit plane with Im z * Im F(z) ≤ 0.
• TauCeti.IsCompleteBernsteinFunction.exists_analyticOnNhd_slitPlane: a complete Bernstein function extends holomorphically to the slit plane with 0 ≤ Im z * Im G(z).

References

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

theorem TauCeti.integrable_inv_add_of_mem_slitPlane {μ : MeasureTheory.Measure NNReal} {z : ℂ} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hz : z ∈ Complex.slitPlane) : MeasureTheory.Integrable (fun (x : NNReal) => (z + ↑↑x)⁻¹) μ

The complex Stieltjes kernel (z + x)⁻¹ is integrable against a measure carrying an integrable Stieltjes weight, at every point z of the slit plane.

theorem TauCeti.hasDerivAt_integral_inv_add {μ : MeasureTheory.Measure NNReal} {z : ℂ} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hz : z ∈ Complex.slitPlane) : HasDerivAt (fun (w : ℂ) => ∫ (x : NNReal), (w + ↑↑x)⁻¹ ∂μ) (-∫ (x : NNReal), ((z + ↑↑x) ^ 2)⁻¹ ∂μ) z

The complex Stieltjes integral is complex differentiable on the slit plane, with derivative -∫ x, (z + x)⁻² ∂μ.

noncomputable def TauCeti.stieltjesExtension (μ : MeasureTheory.Measure NNReal) (a b : NNReal) (z : ℂ) : ℂ

The complex Stieltjes transform of representing data μ, a, b: z ↦ a / z + b + ∫ x, (z + x)⁻¹ ∂μ. It is meaningful on the slit plane ℂ ∖ (-∞, 0], where it is the holomorphic extension of the Stieltjes function represented by μ, a, b.

Equations

• TauCeti.stieltjesExtension μ a b z = ↑↑a / z + ↑↑b + ∫ (x : NNReal), (z + ↑↑x)⁻¹ ∂μ

theorem TauCeti.hasDerivAt_stieltjesExtension {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {z : ℂ} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hz : z ∈ Complex.slitPlane) : HasDerivAt (stieltjesExtension μ a b) (-↑↑a / z ^ 2 - ∫ (x : NNReal), ((z + ↑↑x) ^ 2)⁻¹ ∂μ) z

The complex Stieltjes transform is complex differentiable at every point of the slit plane, with derivative -a / z² - ∫ x, (z + x)⁻² ∂μ.

theorem TauCeti.differentiableOn_stieltjesExtension {μ : MeasureTheory.Measure NNReal} {a b : NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) : DifferentiableOn ℂ (stieltjesExtension μ a b) Complex.slitPlane

The complex Stieltjes transform is complex differentiable on the slit plane.

theorem TauCeti.analyticOnNhd_stieltjesExtension {μ : MeasureTheory.Measure NNReal} {a b : NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) : AnalyticOnNhd ℂ (stieltjesExtension μ a b) Complex.slitPlane

The complex Stieltjes transform is holomorphic on the slit plane.

@[simp]

theorem TauCeti.stieltjesExtension_conj (μ : MeasureTheory.Measure NNReal) (a b : NNReal) (z : ℂ) : stieltjesExtension μ a b ((starRingEnd ℂ) z) = (starRingEnd ℂ) (stieltjesExtension μ a b z)

The complex Stieltjes transform commutes with complex conjugation.

theorem TauCeti.im_stieltjesExtension {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {z : ℂ} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hz : z ∈ Complex.slitPlane) : (stieltjesExtension μ a b z).im = -z.im * (↑a / Complex.normSq z + ∫ (x : NNReal), (Complex.normSq (z + ↑↑x))⁻¹ ∂μ)

The imaginary part of the complex Stieltjes transform: Im F(z) = -Im z * (a / |z|² + ∫ x, |z + x|⁻² ∂μ) on the slit plane.

theorem TauCeti.im_mul_im_stieltjesExtension_nonpos {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {z : ℂ} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hz : z ∈ Complex.slitPlane) : z.im * (stieltjesExtension μ a b z).im ≤ 0

A Stieltjes transform maps the upper half-plane into the closed lower half-plane, and the lower half-plane into the closed upper one: Im z * Im F(z) ≤ 0 on the slit plane.

theorem TauCeti.im_mul_stieltjesExtension {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {z : ℂ} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hz : z ∈ Complex.slitPlane) : (z * stieltjesExtension μ a b z).im = z.im * (↑b + ∫ (x : NNReal), ↑x / Complex.normSq (z + ↑↑x) ∂μ)

The imaginary part of z times the complex Stieltjes transform: Im (z F(z)) = Im z * (b + ∫ x, x / |z + x|² ∂μ) on the slit plane.

theorem TauCeti.im_mul_im_mul_stieltjesExtension_nonneg {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {z : ℂ} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hz : z ∈ Complex.slitPlane) : 0 ≤ z.im * (z * stieltjesExtension μ a b z).im

Im z * Im (z F(z)) ≥ 0 on the slit plane: z ↦ z F(z) maps the upper half-plane into the closed upper half-plane.

theorem TauCeti.stieltjesExtension_eq_zero_iff {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {z : ℂ} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (hz : z ∈ Complex.slitPlane) : stieltjesExtension μ a b z = 0 ↔ a = 0 ∧ b = 0 ∧ μ = 0

The complex Stieltjes transform vanishes only for zero data. At a point of the slit plane, a / z + b + ∫ x, (z + x)⁻¹ ∂μ is zero exactly when a, b and μ all are.

theorem TauCeti.RepresentsStieltjes.stieltjesExtension_ofReal {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) {t : ℝ} (ht : 0 < t) : stieltjesExtension μ a b ↑t = ↑(f t)

The complex Stieltjes transform of a Stieltjes representation of f extends f: it agrees with f on (0, ∞).

theorem TauCeti.RepresentsStieltjes.eqOn_stieltjesExtension {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) {F : ℂ → ℂ} (hF : AnalyticOnNhd ℂ F Complex.slitPlane) (hFf : ∀ (t : ℝ), 0 < t → F ↑t = ↑(f t)) : Set.EqOn F (stieltjesExtension μ a b) Complex.slitPlane

Uniqueness of the holomorphic extension. A function holomorphic on the slit plane that agrees on (0, ∞) with a represented Stieltjes function is its complex Stieltjes transform.

theorem TauCeti.IsStieltjesFunction.exists_analyticOnNhd_slitPlane {f : ℝ → ℝ} (hf : IsStieltjesFunction f) : ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F Complex.slitPlane ∧ (∀ (t : ℝ), 0 < t → F ↑t = ↑(f t)) ∧ ∀ z ∈ Complex.slitPlane, z.im * (F z).im ≤ 0

A Stieltjes function extends holomorphically to the slit plane ℂ ∖ (-∞, 0], and the extension satisfies Im z * Im F(z) ≤ 0: it maps the upper half-plane into the closed lower half-plane.

theorem TauCeti.RepresentsCompleteBernstein.ofReal_mul_stieltjesExtension {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) {t : ℝ} (ht : 0 < t) : ↑t * stieltjesExtension μ a b ↑t = ↑(f t)

On (0, ∞) a complete Bernstein function is t times the complex Stieltjes transform of its representing data.

theorem TauCeti.IsCompleteBernsteinFunction.exists_analyticOnNhd_slitPlane {f : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) : ∃ (G : ℂ → ℂ), AnalyticOnNhd ℂ G Complex.slitPlane ∧ (∀ (t : ℝ), 0 < t → G ↑t = ↑(f t)) ∧ ∀ z ∈ Complex.slitPlane, 0 ≤ z.im * (G z).im

A complete Bernstein function extends holomorphically to the slit plane ℂ ∖ (-∞, 0], and the extension satisfies 0 ≤ Im z * Im G(z): it maps the upper half-plane into the closed upper half-plane.