English
If w lies inside the disk ball around c of radius R, then ∮ z in C(c,R) (z-w)^{-1} dz equals 2πi.
Русский
Если w лежит внутри окружности дискa с центром c и радиусом R, то контурный интеграл (z-w)^{-1} по кругу равен 2πi.
LaTeX
$$$$ \\oint_{z\\in C(c,R)} (z-w)^{-1} \\;dz = 2\\pi i, \\quad \\text{if } w \\in \\mathrm{ball}(c,R). $$$$
Lean4
/-- Integral $\oint_{|z-c|=R} \frac{dz}{z-w} = 2πi$ whenever $|w-c| < R$. -/
theorem integral_sub_inv_of_mem_ball {c w : ℂ} {R : ℝ} (hw : w ∈ ball c R) : (∮ z in C(c, R), (z - w)⁻¹) = 2 * π * I :=
by
have hR : 0 < R := dist_nonneg.trans_lt hw
suffices H : HasSum (fun n : ℕ => ∮ z in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * π * I)
by
have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
refine (H.unique ?_).symm
simpa only [smul_eq_mul, mul_one, add_sub_cancel] using hasSum_two_pi_I_cauchyPowerSeries_integral A hw
have H : ∀ n : ℕ, n ≠ 0 → (∮ z in C(c, R), (z - c) ^ (-n - 1 : ℤ)) = 0 := by
refine fun n hn => integral_sub_zpow_of_ne ?_ _ _ _; simpa
have : (∮ z in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * π * I := by simp [hR.ne']
refine this ▸ hasSum_single _ fun n hn => ?_
simp only [div_eq_mul_inv, mul_pow, integral_const_mul, mul_assoc]
rw [(integral_congr hR.le fun z hz => _).trans (H n hn), mul_zero]
intro z _
rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add, sub_eq_add_neg _ (1 : ℤ)]
