English
If n is an integer with n ≠ −1, then the contour integral of (z−w)^n around the circle equals zero.
Русский
Если n целое и n ≠ −1, то контурный интеграл (z−w)^n по окружности равен нулю.
LaTeX
$$$$\\oint_{z\\in C(c,R)} (z-w)^n\,dz = 0 \\quad \\text{for } n\\in\\mathbb{Z},\\ n\\neq -1.$$$
Lean4
/-- If `n ≠ -1` is an integer number, then the integral of `(z - w) ^ n` over the circle equals
zero. -/
theorem integral_sub_zpow_of_ne {n : ℤ} (hn : n ≠ -1) (c w : ℂ) (R : ℝ) : (∮ z in C(c, R), (z - w) ^ n) = 0 :=
by
rcases em (w ∈ sphere c |R| ∧ n < -1) with (⟨hw, hn⟩ | H)
· exact integral_sub_zpow_of_undef (hn.trans (by decide)) hw
push_neg at H
have hd : ∀ z, z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (n + 1)) ((z - w) ^ n) z :=
by
intro z hne
convert ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const _ using 1
· have hn' : (n + 1 : ℂ) ≠ 0 := by rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
simp [mul_div_cancel_left₀ _ hn']
exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]
refine integral_eq_zero_of_hasDerivWithinAt' fun z hz => (hd z ?_).hasDerivWithinAt
exact (ne_or_eq z w).imp_right fun (h : z = w) => H <| h ▸ hz
