theorem
proved
tactic proof
logDeriv_circle_integral_zero
show as:
view Lean formalization →
formal statement (Lean)
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 :=
proof body
Tactic-mode proof.
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
350 have hball : DifferentiableOn ℂ f (Metric.ball c R) :=
351 _hf_diff.mono Metric.ball_subset_closedBall
352 exact (hball.deriv Metric.isOpen_ball).differentiableAt
353 (Metric.isOpen_ball.mem_nhds hz)
354 exact hderiv_at.div hf_at hf_nz)
355
356/-- Phase charge equals the contour integral winding number for `(z-c)^n`.
357
358The connection: for `f(z) = (z-c)^n`, the winding number integral
359`(2πi)⁻¹ ∮ f'/f dz = (2πi)⁻¹ ∮ n·(z-c)⁻¹ dz = n`, and the
360`ContinuousPhaseData.charge = -n` (sign convention). Thus
361`charge = -(2πi)⁻¹ ∮ f'/f dz`. -/