theorem
proved
term proof
holomorphic_circle_integral_zero
show as:
view Lean formalization →
formal statement (Lean)
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 :=
proof body
Term-mode proof.
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`. -/