Poisson Integral Formula

This file establishes several versions of the Poisson Integral Formula for harmonic 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.

TODO: Extend this formula to vector-valued harmonic functions

theorem InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : HarmonicOnNhd f (Metric.closedBall c R)) (hw : w ∈ Metric.ball c R) : Real.circleAverage (Complex.re ∘ herglotzRieszKernel c w • f) c R = f w

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

theorem InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : HarmonicContOnCl 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 harmonic functions on arbitrary disks in the complex plane, formulated with the real part of the Herglotz–Riesz kernel of integration.

theorem InnerProductSpace.HarmonicOnNhd.circleAverage_poissonKernel_smul {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : HarmonicOnNhd f (Metric.closedBall c R)) (hw : w ∈ Metric.ball c R) : Real.circleAverage (poissonKernel c w • f) c R = f w

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

theorem InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : HarmonicContOnCl 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 harmonic functions on arbitrary disks in the complex plane, formulated with the Poisson kernel of integration.