holomorphic_circle_integral_zero

formal source

 316
 317/-- Cauchy–Goursat for the circle: if `f` is holomorphic on the closed disk
 318(possibly off a countable set), the contour integral vanishes. -/
 319theorem holomorphic_circle_integral_zero {f : ℂ → ℂ} {c : ℂ} {R : ℝ}
 320    (hR : 0 ≤ R)
 321    (hf_cont : ContinuousOn f (Metric.closedBall c R))
 322    (hf_diff : ∀ z ∈ Metric.ball c R, DifferentiableAt ℂ f z) :
 323    (∮ z in C(c, R), f z) = 0 :=
 324  circleIntegral_eq_zero_of_differentiable_on_off_countable hR (s := ∅)
 325    (Set.countable_empty) hf_cont (fun z hz => hf_diff z hz.1)
 326
 327/-- For a holomorphic nonvanishing `f` on the disk, the log-derivative
 328integral vanishes: `∮ f'/f = 0`.
 329
 330This is the contour-integral form of zero winding for holomorphic
 331nonvanishing functions. When `f'/f` is also continuous on the closed
 332disk, this follows directly from Cauchy–Goursat.
 333
 334The key point is differentiability of `f'/f` at interior points, obtained by
 335combining Mathlib's quotient differentiability with differentiability of
 336`deriv f`. -/
 337theorem logDeriv_circle_integral_zero {f : ℂ → ℂ} {c : ℂ} {R : ℝ}
 338    (hR : 0 < R)
 339    (_hf_diff : DifferentiableOn ℂ f (Metric.closedBall c R))
 340    (_hf_nz : ∀ z ∈ Metric.closedBall c R, f z ≠ 0)
 341    (hf'f_cont : ContinuousOn (fun z => deriv f z / f z) (Metric.closedBall c R)) :
 342    (∮ z in C(c, R), (fun z => deriv f z / f z) z) = 0 :=
 343  holomorphic_circle_integral_zero (le_of_lt hR) hf'f_cont
 344    (fun z hz => by
 345      have hf_at : DifferentiableAt ℂ f z :=
 346        (_hf_diff.mono Metric.ball_subset_closedBall).differentiableAt
 347          (Metric.isOpen_ball.mem_nhds hz)
 348      have hf_nz : f z ≠ 0 := _hf_nz z (Metric.ball_subset_closedBall hz)
 349      have hderiv_at : DifferentiableAt ℂ (deriv f) z := by