Theorem InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul

Modification history

2026-03-18 18:34
Mathlib/Analysis/Complex/Harmonic/Poisson.lean
feat: Poisson Integral Formula for harmonic functions (#36278) …
Added InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smulView on Github →