Argument principle

TheoremArgument principle on a closed disc#✓fully proved

Let \(c \in \mathbb{C}\), \(R > 0\), and let \(f : \mathbb{C} \to \mathbb{C}\) be meromorphic on the closed disc \(|z - c| \le R\) with finite order at every point of that disc (so \(f\) vanishes identically near no point). Suppose the order of \(f\) is zero at every point of the circle \(|z - c| = R\). Then the integral of \(f'/f\) over the circle \(|z - c| = R\), traversed once counterclockwise, equals \(2\pi i\) times the sum of the orders of \(f\) at the points of the open disc \(|z - c| < R\) (zeros counted positively and poles negatively, with multiplicity).

theorem argumentPrinciple_closedBall_general
    {c : ℂ} {R : ℝ} (hR : 0 < R)
    {f : ℂ → ℂ}
    (hf : MeromorphicOn f (Metric.closedBall c R))
    (hf_top : ∀ z ∈ Metric.closedBall c R,
      meromorphicOrderAt f z ≠ ⊤)
    (hbd : ∀ z ∈ Metric.sphere c R,
      MeromorphicOn.divisor f (Metric.closedBall c R) z = 0) :
    (∮ z in C(c, R), logDeriv f z) =
      2 * Real.pi * Complex.I *
        ↑(∑ᶠ z, MeromorphicOn.divisor f (Metric.ball c R) z)

Used by 1

Used byArgument principle on a closed disc, with an integrability hypothesis

TheoremArgument principle on a closed disc, with an integrability hypothesis#✓fully proved

Let \(c \in \mathbb{C}\), \(R > 0\), and let \(f : \mathbb{C} \to \mathbb{C}\) be meromorphic on the closed disc \(|z - c| \le R\) with finite order at every point of that disc. Suppose the order of \(f\) is zero at every point of the circle \(|z - c| = R\) and \(f'/f\) is integrable on that circle. Then the integral of \(f'/f\) over the circle, traversed once counterclockwise, equals \(2\pi i\) times the sum of the orders of \(f\) at the points of the open disc \(|z - c| < R\) (zeros counted positively and poles negatively, with multiplicity).

theorem argumentPrinciple_closedBall
    {c : ℂ} {R : ℝ} (hR : 0 < R)
    {f : ℂ → ℂ}
    (hf : MeromorphicOn f (Metric.closedBall c R))
    (hf_top : ∀ z ∈ Metric.closedBall c R,
      meromorphicOrderAt f z ≠ ⊤)
    (hbd : ∀ z ∈ Metric.sphere c R,
      MeromorphicOn.divisor f (Metric.closedBall c R) z = 0)
    (hint : CircleIntegrable (logDeriv f) c R) :
    (∮ z in C(c, R), logDeriv f z) =
      2 * Real.pi * Complex.I *
        ↑(∑ᶠ z, MeromorphicOn.divisor f (Metric.ball c R) z)

Sources

• L. V. Ahlfors, Complex Analysis, 3rd ed., §5.2. It follows from argumentPrinciple_closedBall_general; the hypothesis hint is unused and keeps the source's shape.

Uses 1

Proof usesArgument principle on a closed disc

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.