English
For a circle-integrable f and w inside the open ball (|w|<R), the Cauchy power series sums to the contour integral (2πi)^{-1} ∮ (z-(c+w))^{-1} f(z) dz.
Русский
Для circleIntegrable f и w внутри открытой сферы |w|<R ряд Коши сходится к контурному интегралу (2πi)^{-1} ∮ (z-(c+w))^{-1} f(z) dz.
LaTeX
$$$$ HasSum\\left( n \\mapsto cauchyPowerSeries\\ f\\ c\\ R\\ n\\ f, w\\right) = (2\\pi i)^{-1} \\oint_{|z-c|=R} (z-(c+w))^{-1} f(z) \\,dz. $$$$
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 sum_cauchyPowerSeries_eq_integral {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : CircleIntegrable f c R)
(hw : ‖w‖ < R) : (cauchyPowerSeries f c R).sum w = (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - (c + w))⁻¹ • f z :=
(hasSum_cauchyPowerSeries_integral hf hw).tsum_eq
