English
If n is a negative integer and w lies on the circle of radius |R| about c, then the contour integral of (z−w)^n around that circle is zero.
Русский
Если n — отрицательное целое число и w лежит на окружности с центром c и радиусом |R|, то контурный интеграл (z−w)^n равен нулю вокруг этой окружности.
LaTeX
$$$$\\displaystyle \\text{If } n<0 \\text{ and } w \\in S(c,|R|),\\ then \\\\ \\oint_{z\\in C(c,R)} (z-w)^n \\,dz = 0.$$$$
Lean4
/-- If `n < 0` and `|w - c| = |R|`, then `(z - w) ^ n` is not circle integrable on the circle with
center `c` and radius `|R|`, so the integral `∮ z in C(c, R), (z - w) ^ n` is equal to zero. -/
theorem integral_sub_zpow_of_undef {n : ℤ} {c w : ℂ} {R : ℝ} (hn : n < 0) (hw : w ∈ sphere c |R|) :
(∮ z in C(c, R), (z - w) ^ n) = 0 := by
rcases eq_or_ne R 0 with (rfl | h0)
· apply integral_radius_zero
· apply integral_undef
simpa [circleIntegrable_sub_zpow_iff, *, not_or]
