Commit 2026-03-18 18:34 954b5c55

View on Github →

feat: Poisson Integral Formula for harmonic functions (#36278) Establish two 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. This material is used in Project VD, formalizing Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/Harmonic/Poisson.lean

added theorem InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul

added theorem InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul

added theorem InnerProductSpace.HarmonicOnNhd.circleAverage_poissonKernel_smul

added theorem InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul

Modified Mathlib/Analysis/Complex/Poisson.lean

added theorem herglotzRieszKernel_fun_def