English
The power series associated to a circle about c with radius R expands f around the circle via coefficients given by circle integrals; the coefficients depend only on f∘circleMap, and the series converges to f(w) if f is differentiable on the closed ball, and w lies in the corresponding open ball; for any circle-integrable f it converges to the Cauchy integral of f.
Русский
Связанная с окружностью степень ряда Коши даёт разложение функции вокруг окружности; коэффициенты зависят только от f◦circleMap; ряд сходится к f(w) при дифференцируемости на замкнутом шаре и w внутри открытого шара; для любой circle-integrable f ряд сходится к контурному интегралу.
LaTeX
$$$$\\text{cauchyPowerSeries }(f,c,R) = \\sum_{n=0}^{\\infty} \\text{ContinuousMultilinearMap.mkPiRing } \\Big( (2\\pi i)^{-1} \\oint_{|z-c|=R} \\left(\\frac{w-c}{z-c}\\right)^n \\frac{1}{z-c} f(z)\\,dz \\Big)$$$$
Lean4
/-- The power series that is equal to
$\frac{1}{2πi}\sum_{n=0}^{\infty}
\oint_{|z-c|=R} \left(\frac{w-c}{z - c}\right)^n \frac{1}{z-c}f(z)\,dz$ at
`w - c`. The coefficients of this power series depend only on `f ∘ circleMap c R`, and the power
series converges to `f w` if `f` is differentiable on the closed ball `Metric.closedBall c R` and
`w` belongs to the corresponding open ball. For any circle integrable function `f`, this power
series converges to the Cauchy integral for `f`. -/
def cauchyPowerSeries (f : ℂ → E) (c : ℂ) (R : ℝ) : FormalMultilinearSeries ℂ ℂ E := fun n =>
ContinuousMultilinearMap.mkPiRing ℂ _ <| (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z
