Complex integration, residues and singularities

Contour integrals, Cauchy's theorem, residues, argument principle, Rouché, Laurent series, isolated singularities (Casorati–Weierstrass, great Picard), Schwarz reflection, Looman–Menchoff, normal families and local properties of holomorphic functions on discs and annuli.

TheoremA holomorphic function not identically zero has finitely many zeros in a disc#●ready to prove

Let \(P \in \mathbb{C}\) and \(r > 0\), write \(D(P,r)\) for the open disc and \(\overline{D}(P,r)\) for the closed disc of center \(P\) and radius \(r\), and let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on some open set containing \(\overline{D}(P,r)\). If \(f\) does not vanish identically on \(D(P,r)\), then \(f\) has only finitely many zeros in \(D(P,r)\).

public theorem_wanted finite_zeros_in_ball_of_not_identically_zero
    (f : ℂ → ℂ) (P : ℂ) (r : ℝ) (hr : 0 < r)
    (hhol : ∃ U : Set ℂ, IsOpen U ∧ Metric.closedBall P r ⊆ U ∧ DifferentiableOn ℂ f U)
    (hnot : ¬ ∀ z ∈ Metric.ball P r, f z = 0) :
    (Set.Finite {z : ℂ | z ∈ Metric.ball P r ∧ f z = 0})

Sources

MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l1_26.

TheoremA three-circles inequality for circles tangent at the origin#●ready to prove

Let \(f:\mathbb{C}\to\mathbb{C}\) be an entire function and, for \(r>0\), let [ A(r)=\sup{\lvert f(z)\rvert:\lvert z-r\rvert=r}. ] Then [ A(1)^{2}\le A(2)\,A!\left(\frac{2}{3}\right). ]

public theorem_wanted sq_sSup_norm_circle_one_le_mul
  (f : ℂ → ℂ) (hentire : Differentiable ℂ f)
  (A : ℝ → ℝ) (hA_def : ∀ r : ℝ, 0 < r → A r = sSup {t : ℝ | ∃ z : ℂ, ‖z - r‖ = r ∧ t = ‖f z‖}) :
  A 1 ^ 2 ≤ A 2 * A (2 / 3 : ℝ)

Sources

MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l2_99.

TheoremCasorati–Weierstrass theorem#✓fully proved

Let \(c \in \mathbb{C}\), \(r > 0\), and let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on the punctured disc \(0 < |z - c| < r\) and not meromorphic at \(c\) (that is, \(c\) is neither a removable singularity nor a pole of \(f\)). Then the image of the punctured disc \(0 < |z - c| < r\) under \(f\) is dense in \(\mathbb{C}\).

theorem casoratiWeierstrass
    {c : ℂ} {r : ℝ} {f : ℂ → ℂ} (hr : 0 < r)
    (hf : DifferentiableOn ℂ f (Metric.ball c r \ {c}))
    (hess : ¬ MeromorphicAt f c) :
    Dense (f '' (Metric.ball c r \ {c}))

Sources

L. V. Ahlfors, Complex Analysis, 3rd ed., isolated singularities.

TheoremClassification of isolated singularities#●ready to prove

Let \(c \in \mathbb{C}\), let \(r > 0\), and let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on the punctured disc \(\{z \in \mathbb{C} : 0 < |z - c| < r\}\). Then at least one of the following holds: there is a function \(g\) holomorphic on the disc \(\{z \in \mathbb{C} : |z - c| < r\}\) that agrees with \(f\) on the punctured disc (removable singularity); or \(|f(z)| \to \infty\) as \(z \to c\) with \(z \ne c\) (pole); or for every \(r' > 0\) the image under \(f\) of the punctured disc \(\{z \in \mathbb{C} : 0 < |z - c| < r'\}\) is dense in \(\mathbb{C}\) (essential singularity, Casorati–Weierstrass).

theorem_wanted isolatedSingularity_trichotomy
    {c : ℂ} {r : ℝ} {f : ℂ → ℂ} (hr : 0 < r)
    (hf : DifferentiableOn ℂ f (Metric.ball c r \ {c})) :
    (∃ g : ℂ → ℂ, DifferentiableOn ℂ g (Metric.ball c r) ∧
      Set.EqOn f g (Metric.ball c r \ {c})) ∨
    Filter.Tendsto (fun z => ‖f z‖) (𝓝[≠] c) Filter.atTop ∨
    ∀ r' : ℝ, 0 < r' → Dense (f '' (Metric.ball c r' \ {c}))

Sources

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4, §3.1 and §3.2 (removable singularities; zeros, poles and the Casorati-Weierstrass theorem).

TheoremLaurent expansion on an annulus#●ready to prove

Let \(c \in \mathbb{C}\), let \(r\) and \(R\) be real numbers, and let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on the annulus \(A = \{z \in \mathbb{C} : r < |z - c| < R\}\). Then there are coefficients \(a_n \in \mathbb{C}\) for \(n \in \mathbb{Z}\) such that for every \(z \in A\) the series \(\sum_{n \in \mathbb{Z}} a_n (z - c)^n\) is unconditionally summable with sum \(f(z)\). Here \(0^n = 0\) for \(n < 0\), which matters only at \(z = c\) when \(r < 0\).

theorem_wanted laurentExpansion
    {c : ℂ} {r R : ℝ} {f : ℂ → ℂ}
    (hf : DifferentiableOn ℂ f {z : ℂ | r < ‖z - c‖ ∧ ‖z - c‖ < R}) :
    ∃ a : ℤ → ℂ, ∀ z ∈ {z : ℂ | r < ‖z - c‖ ∧ ‖z - c‖ < R},
      HasSum (fun n : ℤ => a n * (z - c) ^ n) (f z)

Sources

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 5, §1.3 (the Laurent series).

TheoremLooman–Menchoff theorem#✓fully proved

Let \(s \subseteq \mathbb{C}\) be open and let \(f : \mathbb{C} \to \mathbb{C}\) be continuous on \(s\). Write \(u = \operatorname{Re} f\) and \(v = \operatorname{Im} f\) as functions of \(z = x + iy\), and suppose that at every \(z \in s\) the partial derivatives \(u_x(z)\), \(u_y(z)\), \(v_x(z)\), \(v_y(z)\) exist and satisfy the Cauchy–Riemann equations \(u_x(z) = v_y(z)\) and \(u_y(z) = -v_x(z)\). Then \(f\) is complex differentiable on \(s\).

Proof: Baire category gives a square with uniform axis-wise Lipschitz bounds on the exceptional set. A Goursat rectangle estimate and Morera's theorem eliminate that set.

theorem looman_menchoff : ∀ {s : Set ℂ} {f : ℂ → ℂ} {ux uy vx vy : ℂ → ℝ},
    IsOpen s →
    ContinuousOn f s →
    (∀ z ∈ s, HasDerivAt (fun t : ℝ => (f (z + (t : ℂ))).re) (ux z) 0) →
    (∀ z ∈ s, HasDerivAt (fun t : ℝ => (f (z + (t : ℂ) * Complex.I)).re) (uy z) 0) →
    (∀ z ∈ s, HasDerivAt (fun t : ℝ => (f (z + (t : ℂ))).im) (vx z) 0) →
    (∀ z ∈ s, HasDerivAt (fun t : ℝ => (f (z + (t : ℂ) * Complex.I)).im) (vy z) 0) →
    (∀ z ∈ s, ux z = vy z) →
    (∀ z ∈ s, uy z = -(vx z)) →
    DifferentiableOn ℂ f s

Sources

https://en.wikipedia.org/wiki/Looman%E2%80%93Menchoff_theorem (statement id looman-menchoff-s1, canonical name "Looman-Menchoff theorem").

TheoremResidue theorem on a disc#●ready to prove

Let \(c\in\mathbb{C}\) and \(R>0\), and let \(S\) be a finite set of points of the open disc \(\{z:|z-c|\lt R\}\). For each \(s\in S\) let \(r_s>0\) be such that the closed disc \(\{z:|z-s|\le r_s\}\) lies in \(\{z:|z-c|\lt R\}\) and contains no point of \(S\) other than \(s\). Let \(f:\mathbb{C}\to\mathbb{C}\) be complex differentiable on \(\{z:|z-c|\le R\}\setminus S\) and integrable on the circle \(|z-c|=R\) and on each circle \(|z-s|=r_s\). Then, with all circles oriented counterclockwise,

\[\oint_{|z-c|=R} f(z)\,dz=\sum_{s\in S}\oint_{|z-s|=r_s} f(z)\,dz.\]

Each integral on the right is \(2\pi i\) times the residue of \(f\) at \(s\).

theorem_wanted residueTheorem_closedBall
    {c : ℂ} {R : ℝ} (hR : 0 < R)
    {f : ℂ → ℂ} {S : Finset ℂ} {rad : ℂ → ℝ}
    (hS : ∀ s ∈ S, s ∈ Metric.ball c R)
    (hrad : ∀ s ∈ S, 0 < rad s ∧ Metric.closedBall s (rad s) ⊆ Metric.ball c R ∧
      ∀ s' ∈ S, s' ≠ s → s' ∉ Metric.closedBall s (rad s))
    (hf : DifferentiableOn ℂ f (Metric.closedBall c R \ ↑S))
    (hint : CircleIntegrable f c R)
    (hintS : ∀ s ∈ S, CircleIntegrable f s (rad s)) :
    (∮ z in C(c, R), f z) = ∑ s ∈ S, ∮ z in C(s, rad s), f z

Sources

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4, §5.1 (the residue theorem).

TheoremSchwarz reflection principle#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) be holomorphic on the open upper half-plane \(\{z : \operatorname{Im} z > 0\}\), continuous on the closed upper half-plane \(\{z : \operatorname{Im} z \ge 0\}\), and real-valued on the real axis. Then there is an entire function \(g\) that agrees with \(f\) on the closed upper half-plane and satisfies \(g(\bar z) = \overline{g(z)}\) for every \(z \in \mathbb{C}\).

theorem schwarz_reflection :
  ∀ (f : ℂ → ℂ),
    DifferentiableOn ℂ f {z | 0 < z.im} →
      ContinuousOn f {z | 0 ≤ z.im} →
        (∀ z : ℂ, z.im = 0 → (f z).im = 0) →
          ∃ g : ℂ → ℂ,
            DifferentiableOn ℂ g Set.univ ∧
              (∀ z : ℂ, 0 ≤ z.im → g z = f z) ∧
                ∀ z : ℂ, g (star z) = star (g z)

Sources

https://en.wikipedia.org/wiki/Schwarz_reflection_principle.

3 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.