Boundary Cayley coordinates and Nevanlinna measure transport

The boundary Cayley map

x ↦ (x - i) / (x + i)

identifies the real line with the unit circle punctured at 1. This is the boundary counterpart of the Cayley coordinate from the upper half-plane to the unit disc. A finite measure on the circle consequently splits into its atom at 1, which produces the linear term in a Nevanlinna representation, and a finite measure on the real line.

This file gives the explicit boundary homeomorphism and packages the measure transport. The integral decomposition is stated for arbitrary continuous functions on the circle, so it can be applied directly to the Herglotz kernel. Under the boundary coordinate that kernel becomes the Nevanlinna kernel (1 + x * z) / (x - z).

Main declarations

• TauCeti.boundaryCayleyHomeomorph: the homeomorphism from ℝ to Circle \ {1}.
• MeasureTheory.Measure.cayleyPushforward: the finite real-line measure obtained from the non-atomic-at-1 part of a circle measure.
• TauCeti.integral_circle_eq_atom_add_integral_cayleyPushforward: decomposition of an integral over the circle into its atom at 1 and its real-line part.
• TauCeti.nevanlinnaKernel_im, TauCeti.norm_nevanlinnaKernel_le and TauCeti.integrable_nevanlinnaKernel: the imaginary part of the kernel, its boundedness on the real line, and the resulting integrability against a finite measure.
• TauCeti.I_mul_herglotzTransform_cayley_eq: the resulting Nevanlinna-kernel formula for the Cayley-coordinate Herglotz transform.
• TauCeti.nevanlinnaKernel_ofReal: the kernel is real at a real parameter.
• TauCeti.exists_isFiniteMeasure_eq_nevanlinnaKernel_add: the Nevanlinna representation of a Pick function by a nonnegative linear coefficient and a finite real-line measure.

References

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

noncomputable def TauCeti.circleCayleyInv (z : Circle) : ℝ

The real coordinate of a point of the circle. At the omitted point 1 the denominator is zero and Lean's totalized division assigns the harmless value 0; the measure transport below first restricts away from that point.

Equations

• TauCeti.circleCayleyInv z = -(↑z).im / (1 - (↑z).re)

@[simp]

theorem TauCeti.circleCayleyInv_boundaryCayley (x : ℝ) : circleCayleyInv (boundaryCayley x) = x

Applying the real boundary coordinate after the boundary Cayley map gives the original real number.

@[simp]

theorem TauCeti.boundaryCayley_re (x : ℝ) : ((↑x - Complex.I) / (↑x + Complex.I)).re = (x ^ 2 - 1) / (x ^ 2 + 1)

The real part of a boundary Cayley point.

@[simp]

theorem TauCeti.boundaryCayley_im (x : ℝ) : ((↑x - Complex.I) / (↑x + Complex.I)).im = -(2 * x) / (x ^ 2 + 1)

The imaginary part of a boundary Cayley point.

theorem TauCeti.boundaryCayley_circleCayleyInv {z : Circle} (hz : z ≠ 1) : boundaryCayley (circleCayleyInv z) = z

A non-1 point of the circle is recovered from its real boundary coordinate.

theorem TauCeti.continuous_boundaryCayley : Continuous boundaryCayley

The boundary Cayley map is continuous.

theorem TauCeti.measurable_circleCayleyInv : Measurable circleCayleyInv

The inverse boundary coordinate is measurable on the whole circle.

theorem TauCeti.continuous_circleCayleyInv_restrict : Continuous fun (z : { z : Circle // z ≠ 1 }) => circleCayleyInv ↑z

The inverse boundary coordinate is continuous away from the omitted point 1.

noncomputable def TauCeti.boundaryCayleyHomeomorph : ℝ ≃ₜ { z : Circle // z ≠ 1 }

The boundary Cayley homeomorphism from the real line onto the circle punctured at 1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.boundaryCayleyHomeomorph_apply (x : ℝ) : ↑(boundaryCayleyHomeomorph x) = boundaryCayley x

@[simp]

theorem TauCeti.boundaryCayleyHomeomorph_symm_apply (z : { z : Circle // z ≠ 1 }) : boundaryCayleyHomeomorph.symm z = circleCayleyInv ↑z

noncomputable def MeasureTheory.Measure.cayleyPushforward (mu : Measure Circle) : Measure ℝ

The real-line measure obtained by deleting the atom at 1 from a circle measure and pushing the remainder forward through the inverse boundary Cayley coordinate.

Equations

• mu.cayleyPushforward = MeasureTheory.Measure.map TauCeti.circleCayleyInv (mu.restrict {1}ᶜ)

instance MeasureTheory.Measure.isFiniteMeasure_cayleyPushforward (mu : Measure Circle) [IsFiniteMeasure mu] : IsFiniteMeasure mu.cayleyPushforward

The Cayley pushforward of a finite circle measure is finite.

theorem TauCeti.integral_circle_eq_atom_add_integral_cayleyPushforward {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (mu : MeasureTheory.Measure Circle) [MeasureTheory.IsFiniteMeasure mu] (f : Circle → E) (hf : Continuous f) : ∫ (z : Circle), f z ∂mu = mu.real {1} • f 1 + ∫ (x : ℝ), f (boundaryCayley x) ∂mu.cayleyPushforward

Integration against a finite circle measure splits into the contribution of its atom at 1 and integration against its real-line Cayley pushforward.

noncomputable def TauCeti.nevanlinnaKernel (z : ℂ) (x : ℝ) : ℂ

The Nevanlinna kernel on the upper half-plane.

Equations

• TauCeti.nevanlinnaKernel z x = (1 + ↑x * z) / (↑x - z)

theorem TauCeti.nevanlinnaKernel_def (z : ℂ) (x : ℝ) : nevanlinnaKernel z x = (1 + ↑x * z) / (↑x - z)

The Nevanlinna kernel is the quotient (1 + x z) / (x - z).

theorem TauCeti.measurable_nevanlinnaKernel (z : ℂ) : Measurable (nevanlinnaKernel z)

The Nevanlinna kernel is measurable in its real variable at every complex parameter.

theorem TauCeti.nevanlinnaKernel_eq_add_div {z : ℂ} {x : ℝ} (h : ↑x - z ≠ 0) : nevanlinnaKernel z x = z + (1 + z ^ 2) / (↑x - z)

Away from its pole, the Nevanlinna kernel separates into its affine part and a resolvent.

theorem TauCeti.continuousAt_nevanlinnaKernel_left {x : ℝ} {z : ℂ} (h : ↑x ≠ z) : ContinuousAt (fun (w : ℂ) => nevanlinnaKernel w x) z

The Nevanlinna kernel is continuous in its complex parameter away from its pole.

theorem TauCeti.norm_nevanlinnaKernel_le_of_nonpos {z : ℂ} {x : ℝ} (hz : 0 < z.re) (hx : x ≤ 0) : ‖nevanlinnaKernel z x‖ ≤ ‖z‖ + (1 + ‖z‖ ^ 2) / z.re

On the nonpositive real axis, the Nevanlinna kernel is bounded at every parameter with positive real part.

@[simp]

theorem TauCeti.nevanlinnaKernel_ofReal (t x : ℝ) : nevanlinnaKernel (↑t) x = ↑((1 + x * t) / (x - t))

At a real parameter the Nevanlinna kernel is real.

theorem TauCeti.I_mul_herglotzKernel_cayley (z : ℂ) (x : ℝ) (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : Complex.I * ((↑(boundaryCayley x) + (z - Complex.I) / (z + Complex.I)) / (↑(boundaryCayley x) - (z - Complex.I) / (z + Complex.I))) = nevanlinnaKernel z x

In boundary Cayley coordinates, the Herglotz kernel becomes the Nevanlinna kernel.

@[simp]

theorem TauCeti.nevanlinnaKernel_im (z : ℂ) (x : ℝ) : (nevanlinnaKernel z x).im = z.im * (1 + x ^ 2) / Complex.normSq (↑x - z)

The imaginary part of the Nevanlinna kernel. On the upper half-plane it is positive, and the weight 1 + x ^ 2 appearing in the numerator is what turns a Nevanlinna measure into the measure of the Stieltjes--Perron inversion formula.

theorem TauCeti.norm_nevanlinnaKernel_le {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) (x : ℝ) : ‖nevanlinnaKernel z x‖ ≤ (‖z + Complex.I‖ + ‖z - Complex.I‖) / (‖z + Complex.I‖ - ‖z - Complex.I‖)

The Nevanlinna kernel at a point of the upper half-plane is bounded on the real line, by a bound depending only on the distance of the point from the boundary in Cayley coordinates.

theorem TauCeti.continuous_nevanlinnaKernel {z : ℂ} (hz : z.im ≠ 0) : Continuous (nevanlinnaKernel z)

The Nevanlinna kernel at a nonreal point is continuous in the real variable.

theorem TauCeti.integrable_nevanlinnaKernel {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) (mu : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure mu] : MeasureTheory.Integrable (nevanlinnaKernel z) mu

The Nevanlinna kernel at a point of the upper half-plane is integrable against every finite measure on the real line, so the Nevanlinna representation is an honest Bochner integral.

theorem TauCeti.I_mul_herglotzTransform_cayley_eq (mu : MeasureTheory.Measure Circle) [MeasureTheory.IsFiniteMeasure mu] {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : Complex.I * mu.herglotzTransform ((z - Complex.I) / (z + Complex.I)) = ↑(mu.real {1}) * z + ∫ (x : ℝ), nevanlinnaKernel z x ∂mu.cayleyPushforward

Transporting a Cayley-coordinate Herglotz transform to the real line separates the atom at 1 as a nonnegative linear coefficient and writes the remaining term with the Nevanlinna kernel.

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

Nevanlinna representation of a Pick function. A function holomorphic on the upper half-plane with nonnegative imaginary part is the sum of a real constant, a linear term with nonnegative coefficient, and the integral of the Nevanlinna kernel against a finite positive measure on ℝ.

The linear coefficient is the mass at the omitted boundary point 1 of the circle measure in the Cayley-coordinate Herglotz representation.