English
The nth coefficient of the Cauchy power series is the coefficient map applied to w, giving an explicit form for the series as a linear functional in w.
Русский
Нулевой коэффициент ряда Коши описывается как применение коэффициентной карты к w; серия представляет линейный функционал в w.
LaTeX
$$$$ (cauchyPowerSeries\ f\ c\ R\ n)\ (w) = (2\\pi i)^{-1} \\oint_{|z-c|=R} \\left( \\frac{w}{z-c} \\right)^n \\frac{1}{z-c} f(z)\\,dz. $$$$
Lean4
theorem cauchyPowerSeries_apply (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) (w : ℂ) :
(cauchyPowerSeries f c R n fun _ => w) = (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z :=
by
simp only [cauchyPowerSeries, ContinuousMultilinearMap.mkPiRing_apply, Fin.prod_const, div_eq_mul_inv, mul_pow,
mul_smul, circleIntegral.integral_smul]
rw [← smul_comm (w ^ n)]
