def HolomorphicAt (f : ℂ → ℂ) (z₀ : ℂ) : Prop

A complex function $f : \mathbb{C} \to \mathbb{C}$ is holomorphic at $z_0$ if it is complex-differentiable at $z_0$.

def HolomorphicOn (f : ℂ → ℂ) (Ω : Set ℂ) : Prop

A complex function $f$ is holomorphic on an open set $\Omega \subseteq \mathbb{C}$ if it is complex-differentiable at every point of $\Omega$.

def IsEntire (f : ℂ → ℂ) : Prop

A complex function is entire if it is holomorphic on all of $\mathbb{C}$.

theorem theorem_14_24 {Ω : Set ℂ} {f : ℕ → ℂ → ℂ} {g : ℂ → ℂ} (hΩ : IsOpen Ω) (hf : ∀ (n : ℕ), HolomorphicOn (f n) Ω) (hconv : TendstoLocallyUniformlyOn f g Filter.atTop Ω) : HolomorphicOn g Ω

Theorem 14.24 (Weierstrass). A locally uniform limit on an open set $\Omega$ of holomorphic functions is holomorphic on $\Omega$.

theorem liouville_theorem {f : ℂ → ℂ} (hf : IsEntire f) (hb : Bornology.IsBounded (Set.range f)) : ∃ (c : ℂ), f = Function.const ℂ c

Liouville's theorem. A bounded entire function on $\mathbb{C}$ is constant.

def HasZeroOfOrder (k : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) : Prop

$f$ has a zero of order $k$ at $z_0$ if $k > 0$ and locally $f(z) = (z - z_0)^k g(z)$ for some analytic $g$ with $g(z_0) \neq 0$.

def HasPoleOfOrder (k : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) : Prop

$f$ has a pole of order $k$ at $z_0$ iff $1/f$ has a zero of order $k$ at $z_0$.

def HasSimpleZero (f : ℂ → ℂ) (z₀ : ℂ) : Prop

$f$ has a simple zero at $z_0$ if it has a zero of order $1$ there.

def HasSimplePole (f : ℂ → ℂ) (z₀ : ℂ) : Prop

$f$ has a simple pole at $z_0$ if it has a pole of order $1$ there.

theorem hasZeroOfOrder_iff_meromorphicOrderAt {k : ℕ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) : HasZeroOfOrder k f z₀ ↔ 0 < k ∧ meromorphicOrderAt f z₀ = ↑↑k

Compatibility: $f$ has a zero of order $k > 0$ at $z_0$ iff its Mathlib meromorphic order at $z_0$ equals $k$ (as a positive integer).

theorem hasPoleOfOrder_iff_meromorphicOrderAt {k : ℕ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) : HasPoleOfOrder k f z₀ ↔ 0 < k ∧ meromorphicOrderAt f z₀ = ↑(-↑k)

Compatibility: $f$ has a pole of order $k > 0$ at $z_0$ iff its Mathlib meromorphic order at $z_0$ equals $-k$.

def IsMeromorphicOn (f : ℂ → ℂ) (Ω : Set ℂ) : Prop

A function $f$ is meromorphic on an open set $\Omega$ if it is meromorphic at every point of $\Omega$.

theorem isMeromorphicOn_iff {f : ℂ → ℂ} {Ω : Set ℂ} : IsMeromorphicOn f Ω ↔ MeromorphicOn f Ω

IsMeromorphicOn unfolds to Mathlib's MeromorphicOn.

noncomputable def ord (z₀ : ℂ) (f : ℂ → ℂ) : WithTop ℤ

The order of $f$ at $z_0$, in $\mathbb{Z} \cup \{+\infty\}$: positive for zeros, negative for poles, $+\infty$ if $f$ vanishes identically near $z_0$.

structure SmoothCurve : Type

A smooth curve in $\mathbb{C}$: a continuously differentiable map $\gamma : [a, b] \to \mathbb{C}$ on a real interval $[a, b]$.

• a : ℝ
• b : ℝ
• hab : self.a ≤ self.b
• toFun : ℝ → ℂ
• contDiffOn : ContDiffOn ℝ 1 self.toFun (Set.Icc self.a self.b)

@[implicit_reducible]

instance SmoothCurve.instCoeFunForallRealComplex : CoeFun SmoothCurve fun (x : SmoothCurve) => ℝ → ℂ

Coerce a SmoothCurve to its underlying function $[a, b] \to \mathbb{C}$.

def SmoothCurve.image (γ : SmoothCurve) : Set ℂ

The image $\gamma([a, b]) \subseteq \mathbb{C}$ of a smooth curve.

theorem SmoothCurve.continuousOn (γ : SmoothCurve) : ContinuousOn γ.toFun (Set.Icc γ.a γ.b)

A smooth curve is continuous on its parameter interval $[a, b]$.

noncomputable def SmoothCurve.contourIntegral (f : ℂ → ℂ) (γ : SmoothCurve) : ℂ

The contour integral of $f$ along a smooth curve $\gamma$: $\int_\gamma f \, dz = \int_a^b f(\gamma(t)) \gamma'(t) \, dt$.

theorem SmoothCurve.contourIntegral_def (f : ℂ → ℂ) (γ : SmoothCurve) : contourIntegral f γ = ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t

Definitional unfolding of the contour integral along a smooth curve.

structure PiecewiseSmoothCurve : Type

A piecewise smooth curve in $\mathbb{C}$: finitely many smooth pieces $\gamma_0, \dots, \gamma_{n-1}$ glued end-to-end, with matching parameter endpoints and continuous join.

• n : ℕ
• hn : 0 < self.n
• pieces : Fin self.n → SmoothCurve
• endpoints_match (i : Fin self.n) (hi : ↑i + 1 < self.n) : (self.pieces ⟨↑i + 1, hi⟩).a = (self.pieces i).b
• continuous_join (i : Fin self.n) (hi : ↑i + 1 < self.n) : (self.pieces i).toFun (self.pieces i).b = (self.pieces ⟨↑i + 1, hi⟩).toFun (self.pieces ⟨↑i + 1, hi⟩).a

def PiecewiseSmoothCurve.a (γ : PiecewiseSmoothCurve) : ℝ

The starting parameter of a piecewise smooth curve (the $a$ of its first piece).

def PiecewiseSmoothCurve.b (γ : PiecewiseSmoothCurve) : ℝ

The ending parameter of a piecewise smooth curve (the $b$ of its last piece).

noncomputable def PiecewiseSmoothCurve.toFun (γ : PiecewiseSmoothCurve) : ℝ → ℂ

The underlying function $\gamma : \mathbb{R} \to \mathbb{C}$ of a piecewise smooth curve, defined piece-by-piece on the union of the parameter intervals and $0$ outside.

def PiecewiseSmoothCurve.IsSimple (γ : PiecewiseSmoothCurve) : Prop

A piecewise smooth curve is simple if $\gamma$ is injective on the open parameter interval $(a, b)$.

def PiecewiseSmoothCurve.IsClosed (γ : PiecewiseSmoothCurve) : Prop

A piecewise smooth curve is closed if its endpoints coincide: $\gamma(a) = \gamma(b)$.

def PiecewiseSmoothCurve.image (γ : PiecewiseSmoothCurve) : Set ℂ

The image of a piecewise smooth curve in $\mathbb{C}$: the union of the images of its individual smooth pieces.

noncomputable def PiecewiseSmoothCurve.interiorRegion (γ : PiecewiseSmoothCurve) : Set ℂ

The interior region enclosed by a (closed, simple) piecewise smooth curve, in the sense of the Jordan curve theorem.

noncomputable def PiecewiseSmoothCurve.IsPositivelyOriented (γ : PiecewiseSmoothCurve) : Prop

A closed simple piecewise smooth curve is positively oriented if it traverses its image counterclockwise (with the interior on the left).

noncomputable def PiecewiseSmoothCurve.contourIntegral (f : ℂ → ℂ) (γ : PiecewiseSmoothCurve) : ℂ

The contour integral of $f$ along a piecewise smooth curve $\gamma$: the sum of the contour integrals over each smooth piece.

theorem PiecewiseSmoothCurve.contourIntegral_def (f : ℂ → ℂ) (γ : PiecewiseSmoothCurve) : contourIntegral f γ = ∑ i : Fin γ.n, SmoothCurve.contourIntegral f (γ.pieces i)

Definitional unfolding of the contour integral along a piecewise smooth curve.

def SmoothCurve.toPiecewiseSmoothCurve (γ : SmoothCurve) : PiecewiseSmoothCurve

View a smooth curve as a (degenerate) piecewise smooth curve with a single piece.

theorem SmoothCurve.contourIntegral_eq_sub_of_deriv (F : ℂ → ℂ) (γ : SmoothCurve) (hF : ∀ t ∈ Set.uIcc γ.a γ.b, DifferentiableAt ℂ F (γ.toFun t)) (hγ : ∀ t ∈ Set.uIcc γ.a γ.b, DifferentiableAt ℝ γ.toFun t) (hint : IntervalIntegrable (fun (t : ℝ) => deriv F (γ.toFun t) * deriv γ.toFun t) MeasureTheory.volume γ.a γ.b) : contourIntegral (deriv F) γ = F (γ.toFun γ.b) - F (γ.toFun γ.a)

Fundamental theorem of calculus for contour integrals along a smooth curve: if $F$ is complex-differentiable along $\gamma$ and the chain-rule integrand is integrable, then $\int_\gamma F' \, dz = F(\gamma(b)) - F(\gamma(a))$.

theorem PiecewiseSmoothCurve.telescoping_sum (n : ℕ) (hn : 0 < n) (G_b G_a : Fin n → ℂ) (hconnect : ∀ (i : Fin n) (hi : ↑i + 1 < n), G_b i = G_a ⟨↑i + 1, hi⟩) : ∑ i : Fin n, (G_b i - G_a i) = G_b ⟨n - 1, ⋯⟩ - G_a ⟨0, hn⟩

Telescoping sum lemma: if $G^b_i = G^a_{i+1}$ for consecutive indices, then $\sum_{i} (G^b_i - G^a_i) = G^b_{n-1} - G^a_0$.

theorem PiecewiseSmoothCurve.theorem_14_13 (F : ℂ → ℂ) (γ : PiecewiseSmoothCurve) (hF : ∀ (i : Fin γ.n), ∀ t ∈ Set.uIcc (γ.pieces i).a (γ.pieces i).b, DifferentiableAt ℂ F ((γ.pieces i).toFun t)) (hγ : ∀ (i : Fin γ.n), ∀ t ∈ Set.uIcc (γ.pieces i).a (γ.pieces i).b, DifferentiableAt ℝ (γ.pieces i).toFun t) (hint : ∀ (i : Fin γ.n), IntervalIntegrable (fun (t : ℝ) => deriv F ((γ.pieces i).toFun t) * deriv (γ.pieces i).toFun t) MeasureTheory.volume (γ.pieces i).a (γ.pieces i).b) : contourIntegral (deriv F) γ = F ((γ.pieces ⟨γ.n - 1, ⋯⟩).toFun (γ.pieces ⟨γ.n - 1, ⋯⟩).b) - F ((γ.pieces ⟨0, ⋯⟩).toFun (γ.pieces ⟨0, ⋯⟩).a)

Theorem 14.13. Fundamental theorem of calculus for contour integrals along piecewise smooth curves: $\int_\gamma F' \, dz = F(\gamma(b)) - F(\gamma(a))$.

theorem theorem_14_14 (f : ℂ → ℂ) (γ : PiecewiseSmoothCurve) (Ω : Set ℂ) (hΩ : IsOpen Ω) (hf : HolomorphicOn f Ω) (hγ_closed : γ.IsClosed) (hcontained : γ.image ∪ γ.interiorRegion ⊆ Ω) : PiecewiseSmoothCurve.contourIntegral f γ = 0

Theorem 14.14 (Cauchy's theorem). If $f$ is holomorphic on an open set $\Omega$ containing a closed piecewise smooth curve $\gamma$ together with its interior, then $\int_\gamma f \, dz = 0$.

theorem theorem_14_14_circle {R : ℝ} {c : ℂ} {f : ℂ → ℂ} (hR : 0 ≤ R) (hf : DifferentiableOn ℂ f (Metric.closedBall c R)) : ∮ (z : ℂ) in C(c, R), f z = 0

Theorem 14.14 (Cauchy's theorem, circle case). If $f$ is holomorphic on the closed disk $\overline{B(c, R)}$, then its integral around the circle of radius $R$ centred at $c$ vanishes.

noncomputable def Residue.residue (f : ℂ → ℂ) (z₀ : ℂ) : ℂ

The residue $\mathrm{Res}_{z_0}(f)$ of a meromorphic function $f$ at $z_0$, computed via the formula $\frac{1}{(k-1)!} \lim_{z \to z_0} \frac{d^{k-1}}{dz^{k-1}}\bigl[(z - z_0)^k f(z)\bigr]$ for the meromorphic order $k$, and $0$ if $f$ is not meromorphic at $z_0$.

@[simp]

theorem Residue.residue_of_not_meromorphicAt {f : ℂ → ℂ} {z₀ : ℂ} (hf : ¬MeromorphicAt f z₀) : residue f z₀ = 0

The residue is zero when $f$ is not meromorphic at $z_0$.

theorem Residue.residue_eq_zero_of_analyticAt {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) : residue f z₀ = 0

The residue at a regular (analytic) point vanishes.

theorem theorem_14_16 (f : ℂ → ℂ) (γ : PiecewiseSmoothCurve) (Ω : Set ℂ) (N : ℕ) (poles : Fin N → ℂ) (hΩ : IsOpen Ω) (hf_mero : IsMeromorphicOn f Ω) (hγ_closed : γ.IsClosed) (hγ_simple : γ.IsSimple) (hγ_pos : γ.IsPositivelyOriented) (hγ_in_Ω : ∀ (i : Fin γ.n), ∀ t ∈ Set.Icc (γ.pieces i).a (γ.pieces i).b, (γ.pieces i).toFun t ∈ Ω) (hinterior_in_Ω : γ.image ∪ γ.interiorRegion ⊆ Ω) (hpoles_in_interior : ∀ (k : Fin N), poles k ∈ γ.interiorRegion) (hf_holo_off_poles : ∀ z ∈ Ω, (∀ (k : Fin N), z ≠ poles k) → AnalyticAt ℂ f z) (hf_holo_on_curve : ∀ (i : Fin γ.n), ∀ t ∈ Set.Icc (γ.pieces i).a (γ.pieces i).b, AnalyticAt ℂ f ((γ.pieces i).toFun t)) : PiecewiseSmoothCurve.contourIntegral f γ = 2 * ↑Real.pi * Complex.I * ∑ k : Fin N, residue f (poles k)

Theorem 14.16 (Residue theorem). Let $\gamma$ be a positively oriented, simple, closed piecewise smooth curve in an open set $\Omega$ containing $\gamma$ and its interior, and suppose $f$ is meromorphic on $\Omega$ with finitely many poles $p_1, \dots, p_N$ in the interior of $\gamma$. Then $\int_\gamma f \, dz = 2 \pi i \sum_{k=1}^{N} \mathrm{Res}_{p_k}(f)$.

theorem theorem_14_16_circle {R : ℝ} {c : ℂ} (f : ℂ → ℂ) (N : ℕ) (poles : Fin N → ℂ) (hR : 0 < R) (hf_mero : IsMeromorphicOn f (Metric.closedBall c R)) (hpoles_inside : ∀ (k : Fin N), poles k ∈ Metric.ball c R) (hf_holo_off_poles : ∀ z ∈ Metric.closedBall c R, (∀ (k : Fin N), z ≠ poles k) → AnalyticAt ℂ f z) : ∮ (z : ℂ) in C(c, R), f z = 2 * ↑Real.pi * Complex.I * ∑ k : Fin N, residue f (poles k)

Theorem 14.16 (Residue theorem, circle case). For $f$ meromorphic on the closed disk $\overline{B(c, R)}$ with all poles strictly inside, $\oint_{C(c,R)} f \, dz = 2 \pi i \sum_k \mathrm{Res}_{p_k}(f)$.

theorem residue_g_f'_over_f (f g : ℂ → ℂ) (Ω : Set ℂ) (N : ℕ) (zerosAndPoles : Fin N → ℂ) (ordAt : Fin N → ℤ) (hΩ : IsOpen Ω) (hf_mero : IsMeromorphicOn f Ω) (hg_holo : HolomorphicOn g Ω) (hpoints_in_Ω : ∀ (k : Fin N), zerosAndPoles k ∈ Ω) (hord : ∀ (k : Fin N), ord (zerosAndPoles k) f = ↑(ordAt k)) (hf_holo_off_zp : ∀ z ∈ Ω, (∀ (k : Fin N), z ≠ zerosAndPoles k) → AnalyticAt ℂ f z ∧ f z ≠ 0) (k : Fin N) : residue (fun (z : ℂ) => g z * (deriv f z / f z)) (zerosAndPoles k) = g (zerosAndPoles k) * ↑(ordAt k)

The residue of $g \cdot f'/f$ at a zero or pole $p$ of $f$ of order $m$ is $g(p) \cdot m$. (Key ingredient in the argument principle, Theorem 14.17.)

theorem isMeromorphicOn_g_f'_over_f (f g : ℂ → ℂ) (Ω : Set ℂ) (hΩ : IsOpen Ω) (hf_mero : IsMeromorphicOn f Ω) (hg_holo : HolomorphicOn g Ω) : IsMeromorphicOn (fun (z : ℂ) => g z * (deriv f z / f z)) Ω

If $f$ is meromorphic and $g$ is holomorphic on $\Omega$, then the logarithmic-derivative product $g \cdot f'/f$ is meromorphic on $\Omega$.

theorem analyticAt_g_f'_over_f (f g : ℂ → ℂ) (z : ℂ) (Ω : Set ℂ) (hΩ : IsOpen Ω) (hg_holo : HolomorphicOn g Ω) (hz : z ∈ Ω) (hf_an : AnalyticAt ℂ f z) (hf_nz : f z ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => g z * (deriv f z / f z)) z

At a point $z \in \Omega$ where $f$ is analytic and nonvanishing and $g$ is holomorphic, the product $g \cdot f'/f$ is analytic at $z$.

theorem theorem_14_17 (f g : ℂ → ℂ) (γ : PiecewiseSmoothCurve) (Ω : Set ℂ) (N : ℕ) (zerosAndPoles : Fin N → ℂ) (ordAt : Fin N → ℤ) (hΩ : IsOpen Ω) (hf_mero : IsMeromorphicOn f Ω) (hg_holo : HolomorphicOn g Ω) (hγ_closed : γ.IsClosed) (hγ_simple : γ.IsSimple) (hγ_pos : γ.IsPositivelyOriented) (hγ_in_Ω : ∀ (i : Fin γ.n), ∀ t ∈ Set.Icc (γ.pieces i).a (γ.pieces i).b, (γ.pieces i).toFun t ∈ Ω) (hinterior_in_Ω : γ.image ∪ γ.interiorRegion ⊆ Ω) (hpoints_in_interior : ∀ (k : Fin N), zerosAndPoles k ∈ γ.interiorRegion) (hord : ∀ (k : Fin N), ord (zerosAndPoles k) f = ↑(ordAt k)) (hf_holo_off_zp : ∀ z ∈ Ω, (∀ (k : Fin N), z ≠ zerosAndPoles k) → AnalyticAt ℂ f z ∧ f z ≠ 0) (hf_no_zp_on_curve : ∀ (i : Fin γ.n), ∀ t ∈ Set.Icc (γ.pieces i).a (γ.pieces i).b, AnalyticAt ℂ f ((γ.pieces i).toFun t) ∧ f ((γ.pieces i).toFun t) ≠ 0) : PiecewiseSmoothCurve.contourIntegral (fun (z : ℂ) => g z * (deriv f z / f z)) γ = 2 * ↑Real.pi * Complex.I * ∑ k : Fin N, g (zerosAndPoles k) * ↑(ordAt k)

Theorem 14.17 (Generalized argument principle). Let $\gamma$ be a positively oriented, simple, closed piecewise smooth curve in $\Omega$, let $g$ be holomorphic on $\Omega$, and let $f$ be meromorphic on $\Omega$ with no zeros or poles on $\gamma$ and finitely many zeros/poles $p_k$ of order $m_k \in \mathbb{Z}$ inside $\gamma$. Then $\int_\gamma g(z) \frac{f'(z)}{f(z)} \, dz = 2 \pi i \sum_k g(p_k) m_k$.