logDeriv_circle_integral_zero

formal source

 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
 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`. -/
 362theorem zpow_charge_eq_winding_integral (c : ℂ) (R : ℝ) (hR : 0 < R) (n : ℤ) :
 363    ∃ cpd : ContinuousPhaseData,
 364      cpd.center = c ∧ cpd.radius = R ∧ cpd.charge = -n ∧
 365      cpd.charge = -(1 / (2 * ↑π * Complex.I) *
 366        (↑n * ∮ z in C(c, R), (z - c)⁻¹)).re := by
 367  obtain ⟨cpd, hcenter, hradius, hcharge⟩ := zpow_phase_charge c R hR n