English
If f is continuous on a closed disk, differentiable off a countable set inside, and tends to y at the center c, then the contour integral of (z − c)^{-1} f(z) around the circle |z − c| = R equals (2πi) y.
Русский
Пусть f непрерывна на замкнутом диске, дифференцируема вне счётного множества внутри и предел f(z) при z→c существует и равен y; тогда интеграл ∮ (z − c)^{-1} f(z) dz по окружности |z − c| = R равен (2πi) y.
LaTeX
$$$\\oint_{|z-c|=R} (z-c)^{-1} \\cdot f(z) \\, dz = (2 \\pi i) \\cdot y$$$
Lean4
/-- An auxiliary lemma for
`Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable`. This lemma assumes
`w ∉ s` while the main lemma drops this assumption. -/
theorem circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : Set ℂ}
(hs : s.Countable) (hw : w ∈ ball c R \ s) (hc : ContinuousOn f (closedBall c R))
(hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x) : (∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w :=
by
have hR : 0 < R := dist_nonneg.trans_lt hw.1
set F : ℂ → E := dslope f w
have hws : (insert w s).Countable := hs.insert w
have hcF : ContinuousOn F (closedBall c R) := (continuousOn_dslope <| closedBall_mem_nhds_of_mem hw.1).2 ⟨hc, hd _ hw⟩
have hdF : ∀ z ∈ ball (c : ℂ) R \ insert w s, DifferentiableAt ℂ F z := fun z hz =>
(differentiableAt_dslope_of_ne (ne_of_mem_of_not_mem (mem_insert _ _) hz.2).symm).2
(hd _ (diff_subset_diff_right (subset_insert _ _) hz))
have HI := circleIntegral_eq_zero_of_differentiable_on_off_countable hR.le hws hcF hdF
have hne : ∀ z ∈ sphere c R, z ≠ w := fun z hz => ne_of_mem_of_not_mem hz (ne_of_lt hw.1)
have hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R) := fun z hz ↦
calc
F z = (z - w)⁻¹ • (f z - f w) := update_of_ne (hne z hz) ..
_ = (z - w)⁻¹ • f z - (z - w)⁻¹ • f w := smul_sub _ _ _
have hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R) :=
(continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hne z hz
rw [← circleIntegral.integral_sub_inv_of_mem_ball hw.1, ← circleIntegral.integral_smul_const, ← sub_eq_zero, ←
circleIntegral.integral_sub, ← circleIntegral.integral_congr hR.le hFeq, HI]
exacts [(hc'.smul (hc.mono sphere_subset_closedBall)).circleIntegrable hR.le,
(hc'.smul continuousOn_const).circleIntegrable hR.le]
