Documentation

LeanPool.LeanComplexAnalysis.Harmonic.PoissonIntegralCircleAverage

Circle-average Poisson integral formulas #

The upstream ComplexAnalysis/Harmonic/PoissonIntegral_circleAverage.lean file contains circle-average versions of the scaled-disc Poisson integral formulas. In this Lean Pool port, those declarations are provided by LeanPool.LeanComplexAnalysis.Harmonic.PoissonIntegral2.