English
For circle-integrable f and R>0, the Cauchy power series defines a formal multilinear series that converges to the Cauchy integral on the open ball, with radius at least R and with a bound on the sum.
Русский
Для circleIntegrable f и R>0 ряд Коши задаёт формальную многочейловую серию, сходящуюся к контурному интегралу на открытом шаре, с радиусом не меньшим R и оценкой суммы.
LaTeX
$$$$ HasFPowerSeriesOnBall\\left( w \\mapsto (2\\pi i)^{-1} \\oint_{|z-c|=R} (z-w)^{-1} f(z) \\,dz\\right)\\; (cauchyPowerSeries f c R)\\ c\\ R. $$$$
Lean4
/-- For any circle integrable function `f`, the power series `cauchyPowerSeries f c R`, `R > 0`,
converges to the Cauchy integral `(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z` on the open
disc `Metric.ball c R`. -/
theorem hasFPowerSeriesOn_cauchy_integral {f : ℂ → E} {c : ℂ} {R : ℝ≥0} (hf : CircleIntegrable f c R) (hR : 0 < R) :
HasFPowerSeriesOnBall (fun w => (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) (cauchyPowerSeries f c R) c
R :=
{ r_le := le_radius_cauchyPowerSeries _ _ _
r_pos := ENNReal.coe_pos.2 hR
hasSum := fun hy ↦ hasSum_cauchyPowerSeries_integral hf <| by simpa using hy }
