English
Let c ∈ ℂ and 0 < r ≤ R. If a function f: ℂ → E is continuous on the closed annulus r ≤ |z − c| ≤ R and is complex differentiable at all interior points except a countable set, then the contour integral of f(z)/(z − c) around the outer circle |z − c| = R equals the same integral around the inner circle |z − c| = r.
Русский
Пусть c ∈ ℂ и 0 < r ≤ R. Пусть f: ℂ → E непрерывна на замкнутой окружности-кольце r ≤ |z − c| ≤ R и комплексно дифференцируема во всех точках внутренней области, за исключением счётного множества; тогда интеграл по контуру вдоль окружности |z − c| = R от f(z)/(z − c) dz равен такому же интегралу по окружности |z − c| = r.
LaTeX
$$$\\oint_{|z-c|=R} (z-c)^{-1} \\cdot f(z) \\, dz \\,=\\, \\oint_{|z-c|=r} (z-c)^{-1} \\cdot f(z) \\, dz$$$
Lean4
/-- If `f : ℂ → E` is continuous on the closed annulus `r ≤ ‖z - c‖ ≤ R`, `0 < r ≤ R`,
and is complex differentiable at all but countably many points of its interior,
then the integrals of `f z / (z - c)` (formally, `(z - c)⁻¹ • f z`)
over the circles `‖z - c‖ = r` and `‖z - c‖ = R` are equal to each other. -/
theorem circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable {c : ℂ} {r R : ℝ} (h0 : 0 < r)
(hle : r ≤ R) {f : ℂ → E} {s : Set ℂ} (hs : s.Countable) (hc : ContinuousOn f (closedBall c R \ ball c r))
(hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z) :
(∮ z in C(c, R), (z - c)⁻¹ • f z) = ∮ z in C(c, r), (z - c)⁻¹ • f z := by
/- We apply the previous lemma to `fun z ↦ f (c + exp z)` on the rectangle
`[log r, log R] × [0, 2 * π]`. -/
set A := closedBall c R \ ball c r
obtain ⟨a, rfl⟩ : ∃ a, Real.exp a = r := ⟨Real.log r, Real.exp_log h0⟩
obtain ⟨b, rfl⟩ : ∃ b, Real.exp b = R := ⟨Real.log R, Real.exp_log (h0.trans_le hle)⟩
rw [Real.exp_le_exp] at hle
suffices (∫ θ in 0..2 * π, I • f (circleMap c (Real.exp b) θ)) = ∫ θ in 0..2 * π, I • f (circleMap c (Real.exp a) θ)
by
simpa only [circleIntegral, add_sub_cancel_left, ofReal_exp, ← exp_add, smul_smul, ← div_eq_mul_inv,
mul_div_cancel_left₀ _ (circleMap_ne_center (Real.exp_pos _).ne'), circleMap_sub_center, deriv_circleMap]
set R := [[a, b]] ×ℂ [[0, 2 * π]]
set g : ℂ → ℂ := (c + exp ·)
have hdg : Differentiable ℂ g := differentiable_exp.const_add _
replace hs : (g ⁻¹' s).Countable := (hs.preimage (add_right_injective c)).preimage_cexp
have h_maps : MapsTo g R A := by rintro z ⟨h, -⟩; simpa [g, A, dist_eq, norm_exp, hle] using h.symm
replace hc : ContinuousOn (f ∘ g) R := hc.comp hdg.continuous.continuousOn h_maps
replace hd :
∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z :=
by
refine fun z hz => (hd (g z) ⟨?_, hz.2⟩).comp z (hdg _)
simpa [g, dist_eq, norm_exp, hle, and_comm] using hz.1.1
simpa [g, circleMap, exp_periodic _, sub_eq_zero, ← exp_add] using
integral_boundary_rect_eq_zero_of_differentiable_on_off_countable _ ⟨a, 0⟩ ⟨b, 2 * π⟩ _ hs hc hd
