English
When w is inside the disk, the series of coefficients of the Cauchy power series sums to the Cauchy integral with a shifted center: the sum over n of the transformed integrals equals the integral with (z-(c+w))^{-1} times f(z).
Русский
Если w внутри диска, сумма по n коэффициентов ряда Коши равна контурному интегралу с центром смещенным на w: сумма преобразованных интегралов равна интегралу с (z-(c+w))^{-1}·f(z).
LaTeX
$$$$ \\text{HasSum}\\left( n \\mapsto \\oint_{|z-c|=R} \\left( \\frac{w}{z-c} \\right)^n \\frac{1}{z-c} f(z) \\,dz \\right) \\,=\\, \\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` multiplied
by `2πI` converges to the integral `∮ z in C(c, R), (z - w)⁻¹ • f z` on the open disc
`Metric.ball c R`. -/
theorem hasSum_two_pi_I_cauchyPowerSeries_integral {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : CircleIntegrable f c R)
(hw : ‖w‖ < R) :
HasSum (fun n : ℕ => ∮ z in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (∮ z in C(c, R), (z - (c + w))⁻¹ • f z) :=
by
have hR : 0 < R := (norm_nonneg w).trans_lt hw
have hwR : ‖w‖ / R ∈ Ico (0 : ℝ) 1 := ⟨div_nonneg (norm_nonneg w) hR.le, (div_lt_one hR).2 hw⟩
refine
intervalIntegral.hasSum_integral_of_dominated_convergence (fun n θ => ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n)
(fun n => ?_) (fun n => ?_) ?_ ?_ ?_
· simp only [deriv_circleMap]
apply_rules [AEStronglyMeasurable.smul, hf.def'.1] <;> apply Measurable.aestronglyMeasurable
· fun_prop
· fun_prop
· fun_prop
· simp [norm_smul, abs_of_pos hR, mul_left_comm R, inv_mul_cancel_left₀ hR.ne', mul_comm ‖_‖]
· exact Eventually.of_forall fun _ _ => (summable_geometric_of_lt_one hwR.1 hwR.2).mul_left _
· simpa only [tsum_mul_left, tsum_geometric_of_lt_one hwR.1 hwR.2] using hf.norm.mul_continuousOn continuousOn_const
· refine Eventually.of_forall fun θ _ => HasSum.const_smul _ ?_
simp only [smul_smul]
refine HasSum.smul_const ?_ _
have : ‖w / (circleMap c R θ - c)‖ < 1 := by simpa [abs_of_pos hR] using hwR.2
convert (hasSum_geometric_of_norm_lt_one this).mul_right _ using 1
simp [← sub_sub, ← mul_inv, sub_mul, div_mul_cancel₀ _ (circleMap_ne_center hR.ne')]
