English
If f is circle integrable, then the sum of the Cauchy power series equals the Cauchy integral with center shifted by w: sum over n of coefficients equals ∮ (z-(c+w))^{-1} f(z) dz times the appropriate constant.
Русский
Если функция интегрируема по окружности, сумма ряда Коши равна контурному интегралу со смещённым центром на w.
LaTeX
$$$$ (cauchyPowerSeries\\ f\\ c\\ R).sum\\ w = (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 hasSum_cauchyPowerSeries_integral {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : CircleIntegrable f c R)
(hw : ‖w‖ < R) :
HasSum (fun n => cauchyPowerSeries f c R n fun _ => w)
((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - (c + w))⁻¹ • f z) :=
by
simp only [cauchyPowerSeries_apply]
exact (hasSum_two_pi_I_cauchyPowerSeries_integral hf hw).const_smul _
