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.

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))

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

The Poisson kernel of integration.

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.

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.