Poisson Integral Formula

We present two versions of the Poisson Integral Formula for ℂ-differentiable functions on arbitrary disks in the complex plane, formulated with the real part of the Herglotz–Riesz kernel of integration and with the Poisson kernel, respectively.

Kernels of Integration

For convenience, this preliminary section discussed the kernels on integration that appear in the various versions of the Poisson Formula.

noncomputable def herglotzRieszKernel (c w z : ℂ) : ℂ

The Herglotz-Riesz kernel of integration.

Equations

• herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))

theorem herglotzRieszKernel_def (c w z : ℂ) : herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))

theorem herglotzRieszKernel_fun_def (c w : ℂ) : herglotzRieszKernel c w = fun (z : ℂ) => (z - c + (w - c)) / (z - c - (w - c))

theorem herglotzRieszKernel_add_const (c w z : ℂ) : herglotzRieszKernel c w (z + c) = herglotzRieszKernel 0 (w - c) z

noncomputable def poissonKernel (c w z : ℂ) : ℝ

The Poisson kernel of integration.

Equations

• poissonKernel c w z = (‖z - c‖ ^ 2 - ‖w - c‖ ^ 2) / ‖z - c - (w - c)‖ ^ 2

theorem poissonKernel_def (c w z : ℂ) : poissonKernel c w z = (‖z - c‖ ^ 2 - ‖w - c‖ ^ 2) / ‖z - c - (w - c)‖ ^ 2

theorem poissonKernel_eq_re_herglotzRieszKernel {c w : ℂ} : poissonKernel c w = Complex.re ∘ herglotzRieszKernel c w

Companion theorem to the Poisson Integral Formula: The real part of the Herglotz–Riesz kernel and the Poisson kernel agree on the path of integration.

theorem re_herglotzRieszKernel_le {R : ℝ} {w c z : ℂ} (hz : z ∈ Metric.sphere c R) (hw : w ∈ Metric.ball c R) : ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (R + ‖w - c‖) / (R - ‖w - c‖)

Companion theorem to the Poisson Integral Formula: Upper estimate for the real part of the Herglotz-Riesz kernel.

theorem le_re_herglotzRieszKernel {R : ℝ} {w c z : ℂ} (hz : z ∈ Metric.sphere c R) (hw : w ∈ Metric.ball c R) : (R - ‖w - c‖) / (R + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re

Companion theorem to the Poisson Integral Formula: Lower estimate for the real part of the Herglotz-Riesz kernel.

theorem continuousOn_herglotzRieszKernel_sphere {R : ℝ} {w c : ℂ} (hw : w ∈ Metric.ball c R) : ContinuousOn (herglotzRieszKernel c w) (Metric.sphere c |R|)

The Herglotz–Riesz kernel herglotzRieszKernel c w is continuous on the circle sphere c |R| whenever w ∈ ball c R.

theorem re_circleAverage_herglotzRieszKernel_smul {R : ℝ} {w : ℂ} {g : ℂ → ℝ} (hg : CircleIntegrable g 0 R) (hw : w ∈ Metric.ball 0 R) : (Real.circleAverage (fun (ζ : ℂ) => herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R).re = Real.circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • g) 0 R

Taking real parts commutes with the Herglotz–Riesz kernel integral of a real-valued circle-integrable function.

Integral Formulas

theorem DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E] {c : ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hw : w ∈ Metric.ball c R) : Real.circleAverage (Complex.re ∘ herglotzRieszKernel c w • f) c R = f w

Poisson integral formula for ℂ-differentiable functions on arbitrary disks in the complex plane, formulated with the real part of the Herglotz–Riesz kernel of integration.

theorem DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E] {c : ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hw : w ∈ Metric.ball c R) : Real.circleAverage (fun (z : ℂ) => ((z - c + (w - c)) / (z - c - (w - c))).re • f z) c R = f w

Poisson integral formula for ℂ-differentiable functions on arbitrary disks in the complex plane, formulated with the real part of the Herglotz–Riesz kernel of integration expanded.

theorem DiffContOnCl.circleAverage_poissonKernel_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E] {c : ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hw : w ∈ Metric.ball c R) : Real.circleAverage (poissonKernel c w • f) c R = f w

Poisson integral formula for ℂ-differentiable functions on arbitrary disks in the complex plane, formulated with the Poisson kernel of integration.

theorem DiffContOnCl.circleAverage_poissonKernel_smul' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E] {c : ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hw : w ∈ Metric.ball c R) : Real.circleAverage (fun (z : ℂ) => ((‖z - c‖ ^ 2 - ‖w - c‖ ^ 2) / ‖z - c - (w - c)‖ ^ 2) • f z) c R = f w

Poisson integral formula for ℂ-differentiable functions on arbitrary disks in the complex plane, formulated with the Poisson kernel of integration expanded.

Derivative of the Herglotz–Riesz Kernel Integral

theorem hasDerivAt_circleAverage_herglotzRieszKernel_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} (hg : CircleIntegrable f 0 R) (hw : w ∈ Metric.ball 0 R) : HasDerivAt (fun (w : ℂ) => Real.circleAverage (fun (ζ : ℂ) => herglotzRieszKernel 0 w ζ • f ζ) 0 R) (Real.circleAverage (fun (ζ : ℂ) => (2 * ζ / (ζ - w) ^ 2) • f ζ) 0 R) w

Derivative of the Herglotz–Riesz kernel integral: if f is circle integrable and w lies inside the circle, then w ↦ circleAverage (fun ζ ↦ herglotzRieszKernel 0 w ζ • f ζ) 0 R has derivative circleAverage (fun ζ ↦ (2 * ζ / (ζ - w) ^ 2) • f ζ) 0 R at w.

theorem differentiableOn_circleAverage_herglotzRieszKernel_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} (hg : CircleIntegrable f 0 R) : DifferentiableOn ℂ (fun (w : ℂ) => Real.circleAverage (fun (ζ : ℂ) => herglotzRieszKernel 0 w ζ • f ζ) 0 R) (Metric.ball 0 R)

The Herglotz–Riesz kernel integral of a circle-integrable function is differentiable in the pole parameter, throughout the open ball.

theorem analyticOnNhd_circleAverage_herglotzRieszKernel_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} [CompleteSpace E] (hg : CircleIntegrable f 0 R) : AnalyticOnNhd ℂ (fun (w : ℂ) => Real.circleAverage (fun (ζ : ℂ) => herglotzRieszKernel 0 w ζ • f ζ) 0 R) (Metric.ball 0 R)

The Herglotz–Riesz kernel integral of a circle-integrable function is analytic in the pole parameter, throughout the open ball.