Complex analysis · The Lumenary

MotivationH

One derivative, and everything follows

Here is a real integral that resists every technique of first-year calculus:

\int_{-\infty}^{\infty} \frac{\cos x}{1 + x^2}\,dx = \frac{\pi}{e}.

The integrand has no elementary antiderivative. Yet a complex analyst evaluates it in three lines, by walking around a semicircle in the complex plane and computing one number at the point $z = i$ . The same method counts the zeros of a polynomial inside a circle without finding them. It proves that every polynomial has a complex root, and it is the engine behind the prime number theorem.

All of this comes from a definition that looks harmless: a function $f$ of a complex variable is holomorphic if the limit

f'(z) = \lim_{h \to 0} \frac{f(z + h) - f(z)}{h}

exists, where now $h$ is a complex number that may approach $0$ from any direction. That one requirement is far stronger than it looks. A real function can be differentiable once and not twice. A holomorphic function is automatically differentiable infinitely often and equal to its Taylor series. It is determined everywhere by its values on a tiny segment, and inside a disc it is determined by its values on the boundary circle. Engineers use the same functions to map the flow of air around a circle onto the flow around an aeroplane wing.

This lesson builds the theory from the definition: the Cauchy–Riemann equations, contour integrals, Cauchy's theorem and integral formula, power series, Liouville's theorem, the fundamental theorem of algebra, and the residue theorem.

IntuitionH

Derivatives that rotate and stretch

A real-differentiable map of the plane looks, near a point, like a linear map $\R^2 \to \R^2$ — any $2 \times 2$ matrix. A complex derivative $f'(z_0) = re^{i\theta}$ says much more: near $z_0$ , $f$ acts like multiplication by $f'(z_0)$ , that is, a rotation by $\theta$ combined with scaling by $r$ . Rotations-with-scaling are the matrices

\begin{pmatrix} a & -b \\ b & a \end{pmatrix}, \qquad a + ib = f'(z_0).

So a holomorphic map, wherever $f' \ne 0$ , turns tiny squares into tiny squares. It may rotate and resize them, but it never shears them or flips them over. It preserves angles and orientation: it is conformal. Complex conjugation $z \mapsto \bar z$ is a reflection, the matrix $\mathrm{diag}(1, -1)$ . It is perfectly smooth as a map of the plane, but it reverses orientation, so it is not complex-differentiable anywhere.

The second picture is the contour integral. Walking once around the origin, $\oint dz/z = 2\pi i$ measures how far the argument of $z$ turns: one full turn, $2\pi$ . For a function holomorphic inside the loop, the corresponding integral is $0$ . Cauchy's theorem says that integrals of holomorphic functions only notice the holes the path goes around. That is why complex analysis is secretly topology.

DefinitionsH

Definitions

Definition— complex derivative, holomorphic, entire

Let $U \subseteq \C$ be open and $f : U \to \C$ . $f$ is complex-differentiable at $z_0 \in U$ if $f'(z_0) = \lim_{h \to 0,\ h \in \C} \frac{f(z_0 + h) - f(z_0)}{h}$ exists. $f$ is holomorphic on $U$ if it is complex-differentiable at every point of $U$ , and entire if it is holomorphic on $\C$ .

Sums, products, quotients (where the denominator is non-zero) and composites of holomorphic functions are holomorphic, with the usual rules, by the same proofs as in real calculus. Polynomials are entire, and so are $e^z = \sum z^n/n!$ , $\sin z$ and $\cos z$ .

Definition— contour integral

A path is a piecewise continuously differentiable map $\gamma : [a, b] \to \C$ ; it is closed if $\gamma(a) = \gamma(b)$ . For $f$ continuous on the image of $\gamma$ ,

\int_\gamma f(z)\,dz = \int_a^b f(\gamma(t))\,\gamma'(t)\,dt.

The circle $|z - c| = R$ traversed once anticlockwise, $\gamma(t) = c + Re^{it}$ for $t \in [0, 2\pi]$ , gives $\oint_{|z - c| = R} f(z)\,dz$ .

Two facts are used constantly. The ML-inequality: if $|f| \le M$ on the image of $\gamma$ and $\gamma$ has length $L$ , then $\left|\int_\gamma f\right| \le ML$ . And primitives kill closed integrals: if $F' = f$ on an open set containing the image of $\gamma$ , then $\int_\gamma f = F(\gamma(b)) - F(\gamma(a))$ , which is $0$ for closed $\gamma$ (chain rule plus the real fundamental theorem of calculus).

Definition— isolated singularity, pole, residue

If $f$ is holomorphic on a punctured disc $0 < |z - a| < r$ , then $a$ is an isolated singularity. It is removable if $f$ extends holomorphically to $a$ . It is a pole of order $m \ge 1$ if $f(z) = g(z)/(z - a)^m$ with $g$ holomorphic near $a$ and $g(a) \ne 0$ . Otherwise it is essential. The residue $\operatorname{Res}_a f$ is the coefficient $c_{-1}$ of $(z - a)^{-1}$ in the Laurent expansion $f(z) = \sum_{n \in \Z} c_n (z - a)^n$ about $a$ .

Definition— winding number

For a closed path $\gamma$ and a point $w$ not on it, the winding number is $n(\gamma, w) = \frac{1}{2\pi i} \int_\gamma \frac{dz}{z - w}$ . It is an integer, and it counts the number of times $\gamma$ travels anticlockwise around $w$ .

Worked examplesH

Examples and non-examples

Example— The integral of (z − c) to the power n

Parametrise $z = c + Re^{it}$ , so $dz = iRe^{it}\,dt$ . For every integer $n$ ,

\oint_{|z - c| = R} (z - c)^n\,dz = \int_0^{2\pi} R^n e^{int}\, iRe^{it}\,dt = iR^{n+1} \int_0^{2\pi} e^{i(n+1)t}\,dt = \begin{cases} 2\pi i & n = -1, \\ 0 & n \ne -1. \end{cases}

For $n \ne -1$ this also follows from the primitive $(z - c)^{n+1}/(n+1)$ . For $n = -1$ there is no primitive on $\C \setminus \{c\}$ : a "logarithm" would have to increase by $2\pi i$ every time it goes around $c$ . This single computation is the seed of the residue theorem.

Example— Real-differentiable is not enough

Write $z = x + iy$ . The map $f(z) = \bar z = x - iy$ is linear over $\R$ , hence real-differentiable. But along a real increment $h = t$ the difference quotient is $\bar t/t = 1$ , and along an imaginary increment $h = it$ it is $\overline{it}/(it) = -1$ . The limit does not exist, so $\bar z$ is complex-differentiable nowhere. Similarly $|z|^2 = z\bar z$ is complex-differentiable only at $0$ , and $\operatorname{Re} z$ nowhere. Consistently, $\oint_{|z| = 1} \bar z\,dz = \oint dz/z = 2\pi i \ne 0$ , since $\bar z = 1/z$ on the unit circle.

Example— Three kinds of isolated singularity

$\frac{\sin z}{z}$ at $0$ : removable, since $\frac{\sin z}{z} = 1 - \frac{z^2}{3!} + \frac{z^4}{5!} - \cdots$ extends with value $1$ .
$\frac{1}{z^2 + 1}$ at $i$ : a simple pole, $\frac{1}{(z - i)(z + i)}$ , with residue $\frac{1}{2i}$ .
$e^{1/z} = \sum_{n \ge 0} \frac{1}{n!\,z^n}$ at $0$ : essential, with infinitely many negative powers and residue $1$ . Near $0$ it takes every non-zero value infinitely often (a theorem of Picard).

ProofH

The Cauchy–Riemann equations

Theorem— Theorem 1 (Cauchy–Riemann)

Write $f = u + iv$ with $u, v$ real-valued functions of $(x, y)$ . If $f$ is complex-differentiable at $z_0 = x_0 + iy_0$ , then the partial derivatives of $u$ and $v$ exist at $(x_0, y_0)$ and

u_x = v_y, \qquad u_y = -v_x, \qquad f'(z_0) = u_x + iv_x.

Conversely, if $u$ and $v$ have continuous partial derivatives near $(x_0, y_0)$ satisfying these equations there, then $f$ is holomorphic near $z_0$ .

Proof

Let $h \to 0$ along the real axis, $h = t \in \R$ : the difference quotient tends to $u_x + iv_x$ , which must equal $f'(z_0)$ . Along the imaginary axis, $h = it$ :

\frac{f(z_0 + it) - f(z_0)}{it} = \frac{1}{i}\left( \frac{u(x_0, y_0 + t) - u(x_0, y_0)}{t} + i\,\frac{v(x_0, y_0 + t) - v(x_0, y_0)}{t} \right) \to -iu_y + v_y.

Equating real and imaginary parts of $u_x + iv_x = v_y - iu_y$ gives the equations.

Conversely, continuous partial derivatives make $(u, v)$ real-differentiable: $f(z_0 + h) - f(z_0) = A h + o(|h|)$ , where $A$ is the Jacobian matrix acting on $h = (h_1, h_2)$ . The equations say $A = \begin{pmatrix} a & -b \\ b & a \end{pmatrix}$ with $a = u_x$ , $b = v_x$ , and this matrix acts on $h_1 + ih_2$ as multiplication by $a + ib$ . So $\frac{f(z_0 + h) - f(z_0)}{h} = (a + ib) + o(1)$ .

∎

The equations have a striking consequence. If $u, v$ are twice continuously differentiable (we shall see that they always are), then $u_{xx} + u_{yy} = v_{yx} - v_{xy} = 0$ . The real and imaginary parts of a holomorphic function are harmonic. For example, $z^2 = (x^2 - y^2) + i(2xy)$ , and both $x^2 - y^2$ and $2xy$ satisfy Laplace's equation.

ProofH

Cauchy's theorem and the integral formula

Theorem— Theorem 2 (Goursat)

If $f$ is holomorphic on an open set containing a closed triangle $T$ (with its inside), then $\oint_{\partial T} f(z)\,dz = 0$ .

Proof

Let $I = \left|\oint_{\partial T} f\right|$ , and let $p$ and $d$ be the perimeter and diameter of $T$ . Join the midpoints of the sides to cut $T$ into four similar triangles. The integrals over their boundaries add up to the integral over $\partial T$ , because the inner edges are traversed twice in opposite directions. So one of them, $T_1$ , has $\left|\oint_{\partial T_1} f\right| \ge I/4$ . Repeating gives nested triangles $T \supset T_1 \supset T_2 \supset \cdots$ with

\left|\oint_{\partial T_n} f\right| \ge 4^{-n} I, \qquad \text{perimeter } 2^{-n} p, \qquad \text{diameter } 2^{-n} d.

By completeness (the nested compact sets have a common point) there is $z_0 \in \bigcap T_n$ . Since $f$ is differentiable at $z_0$ , $f(z) = f(z_0) + f'(z_0)(z - z_0) + \psi(z)(z - z_0)$ with $\psi(z) \to 0$ as $z \to z_0$ . The linear part has a primitive, so its integral over $\partial T_n$ vanishes. Let $\varepsilon_n = \sup_{T_n} |\psi|$ , so $\varepsilon_n \to 0$ . By the ML-inequality,

4^{-n} I \le \left|\oint_{\partial T_n} \psi(z)(z - z_0)\,dz\right| \le \varepsilon_n \cdot 2^{-n} d \cdot 2^{-n} p.

So $I \le \varepsilon_n\, dp \to 0$ , and $I = 0$ .

∎

Theorem— Lemma 3 (one exceptional point)

Goursat's theorem still holds if $f$ is continuous on the open set and holomorphic except at one point $w$ .

Proof

If $w$ is a vertex of $T$ , cut off a tiny triangle at $w$ of perimeter $\eta$ . The rest of $T$ splits into triangles not containing $w$ , whose integrals vanish by Theorem 2. The tiny triangle contributes at most $\eta \cdot \sup_T |f|$ , which tends to $0$ with $\eta$ . If $w$ lies elsewhere in $T$ , split $T$ into triangles that have $w$ as a vertex.

∎

Theorem— Theorem 4 (Cauchy's theorem in a disc)

Let $f$ be continuous on an open disc $D$ and holomorphic on $D$ except possibly at one point. Then $f$ has a primitive on $D$ , and $\int_\gamma f\,dz = 0$ for every closed path $\gamma$ in $D$ .

Proof

Let $c$ be the centre and set $F(z) = \int_{[c, z]} f$ , the integral along the segment from $c$ to $z$ . For $z, z + h \in D$ , Lemma 3 for the triangle with vertices $c, z, z + h$ gives $F(z + h) - F(z) = \int_{[z, z + h]} f$ . Since $\int_{[z, z + h]} f(z)\,d\zeta = h f(z)$ ,

\left| \frac{F(z + h) - F(z)}{h} - f(z) \right| = \left| \frac{1}{h} \int_{[z, z + h]} \big(f(\zeta) - f(z)\big)\,d\zeta \right| \le \sup_{\zeta \in [z, z + h]} |f(\zeta) - f(z)| \to 0

by continuity. So $F' = f$ , and integrals of $f$ over closed paths vanish because $f$ has a primitive.

∎

Note

Cauchy's theorem holds far beyond discs. General form (stated, not proved here): if $f$ is holomorphic on an open set $U$ and the closed path $\gamma$ in $U$ is null-homotopic in $U$ — or more generally has winding number $0$ about every point outside $U$ — then $\int_\gamma f = 0$ . In particular this holds for every closed path in a simply connected domain. See Ahlfors (1979), chapter 4, or Stein and Shakarchi (2003), chapter 3. In this lesson we use only discs and circles.

Theorem— Lemma 5

If $|w - c| < R$ , then $\displaystyle \oint_{|z - c| = R} \frac{dz}{z - w} = 2\pi i$ .

Proof

On the circle $|w - c| / |z - c| = |w - c|/R =: q < 1$ , so the geometric series

\frac{1}{z - w} = \frac{1}{(z - c)\big(1 - \frac{w - c}{z - c}\big)} = \sum_{n \ge 0} \frac{(w - c)^n}{(z - c)^{n+1}}

converges uniformly on the circle (M-test with $M_n = q^n/R$ ). Integrate term by term: by the first example, only $n = 0$ survives, giving $2\pi i$ .

∎

Theorem— Theorem 6 (Cauchy's integral formula)

Let $f$ be holomorphic on an open set containing the closed disc $|z - c| \le R$ . Then for every $w$ with $|w - c| < R$ ,

f(w) = \frac{1}{2\pi i} \oint_{|z - c| = R} \frac{f(z)}{z - w}\,dz.

Proof

$f$ is holomorphic on a slightly larger disc $D$ . Define $g(z) = \frac{f(z) - f(w)}{z - w}$ for $z \ne w$ and $g(w) = f'(w)$ . Then $g$ is continuous on $D$ and holomorphic except at $w$ , so $\oint g = 0$ by Theorem 4. Hence

\oint \frac{f(z)}{z - w}\,dz = f(w) \oint \frac{dz}{z - w} = 2\pi i\, f(w)

by Lemma 5.

∎

The values of a holomorphic function inside a disc are determined by its values on the boundary. Nothing like this is true for real-differentiable functions.

ProofH

Power series, Liouville and the fundamental theorem of algebra

Theorem— Theorem 7 (holomorphic functions are analytic)

Let $f$ be holomorphic on the open disc $|z - c| < \rho$ . Then $f(w) = \sum_{n \ge 0} a_n (w - c)^n$ for all $|w - c| < \rho$ , where, for any $0 < R < \rho$ ,

a_n = \frac{1}{2\pi i} \oint_{|z - c| = R} \frac{f(z)}{(z - c)^{n+1}}\,dz.

Consequently $f$ is infinitely complex-differentiable, with $f^{(n)}(c) = n!\,a_n$ .

Proof

Fix $w$ and choose $R$ with $|w - c| < R < \rho$ . Substitute the uniformly convergent geometric series of Lemma 5 into Cauchy's formula. Uniform convergence allows term-by-term integration (the ML-inequality bounds the tail by $2\pi R \cdot \sup|f| \cdot \sum_{n > N} q^n/R$ ), and this gives the series. A power series is infinitely differentiable inside its disc of convergence, with derivatives computed term by term, so $f^{(n)}(c) = n!\,a_n$ . The coefficients do not depend on $R$ , because they are determined by the derivatives at $c$ .

∎

So the Taylor series of a holomorphic function converges on the largest disc on which the function is holomorphic. That explains a real-analysis puzzle. The Taylor series of $\frac{1}{1 + x^2}$ about $0$ has radius $1$ , although the function is perfectly smooth on all of $\R$ . Over $\C$ it has poles at $\pm i$ , at distance $1$ .

Theorem— Corollary 8 (Cauchy's estimates)

If $f$ is holomorphic on a neighbourhood of $|z - c| \le R$ and $|f| \le M$ on the circle $|z - c| = R$ , then $|f^{(n)}(c)| \le n!\,M / R^n$ .

Proof

ML-inequality in the formula for $a_n$ : $|a_n| \le \frac{1}{2\pi} \cdot 2\pi R \cdot \frac{M}{R^{n+1}} = \frac{M}{R^n}$ .

∎

Theorem— Theorem 9 (Liouville)

Every bounded entire function is constant.

Proof

If $|f| \le M$ on $\C$ , Corollary 8 with $n = 1$ gives $|f'(c)| \le M/R$ for every $R > 0$ , so $f'(c) = 0$ for every $c$ . A function with zero derivative on the connected set $\C$ is constant (integrate along segments from $0$ ).

∎

Theorem— Theorem 10 (fundamental theorem of algebra)

Every non-constant polynomial $p$ with complex coefficients has a complex root. Hence $p$ factors as $c\prod_{k=1}^n (z - z_k)$ .

Proof

Write $p(z) = a_n z^n + \cdots + a_0$ with $n \ge 1$ and $a_n \ne 0$ . For $|z| \ge R_0 := \max\big(1, 2\sum_{k < n} |a_k| / |a_n|\big)$ we have $|p(z)| \ge |a_n||z|^n - \sum_{k<n} |a_k||z|^{n-1} \ge \tfrac12 |a_n| |z|^n$ , so $|p(z)| \to \infty$ . Suppose $p$ had no root. Then $1/p$ is entire. It is bounded by $2/|a_n|$ for $|z| \ge R_0$ , and bounded on the compact disc $|z| \le R_0$ by continuity. By Liouville, $1/p$ is constant, so $p$ is constant — a contradiction. The factorisation follows by induction on the degree, dividing by $z - z_1$ .

∎

ProofH

Laurent series and the residue theorem

Theorem— Proposition 11 (principal parts)

Let $f$ have a pole of order $m$ at $a$ : $f(z) = g(z)/(z - a)^m$ with $g$ holomorphic near $a$ , $g(a) \ne 0$ . Expanding $g(z) = \sum_{k \ge 0} b_k (z - a)^k$ (Theorem 7) gives

f(z) = \underbrace{\frac{b_0}{(z - a)^m} + \cdots + \frac{b_{m-1}}{z - a}}_{\text{principal part } P_a(z)} + \sum_{k \ge 0} b_{m + k}(z - a)^k,

so $f - P_a$ is holomorphic near $a$ (after removing the singularity), and $\operatorname{Res}_a f = b_{m-1} = \frac{g^{(m-1)}(a)}{(m-1)!}$ . For a simple pole of a quotient $f = \phi/\psi$ with $\psi(a) = 0 \ne \psi'(a)$ and $\phi(a) \ne 0$ : $\operatorname{Res}_a f = \phi(a)/\psi'(a)$ .

(Every isolated singularity, including essential ones, has a two-sided Laurent expansion $\sum_{n \in \Z} c_n (z - a)^n$ on a punctured disc, proved like Theorem 7 on an annulus. We will only need poles.)

Theorem— Theorem 12 (residue theorem for a disc)

Let $f$ be holomorphic on an open set containing the closed disc $|z - c| \le R$ , except at finitely many poles $a_1, \dots, a_k$ , all with $|a_j - c| < R$ . Then

\oint_{|z - c| = R} f(z)\,dz = 2\pi i \sum_{j=1}^k \operatorname{Res}_{a_j} f.

Proof

Let $P_j$ be the principal part at $a_j$ . The function $h = f - \sum_j P_j$ has only removable singularities in the disc. Each $P_\ell$ is holomorphic away from $a_\ell$ , and $f - P_j$ is holomorphic near $a_j$ by Proposition 11. After removing those singularities, $h$ is holomorphic on a disc slightly larger than $|z - c| \le R$ . By Theorem 4, $\oint h = 0$ . And $\oint P_j = \sum_n b^{(j)}_n \oint (z - a_j)^{-n}\,dz$ , where only the term $(z - a_j)^{-1}$ survives, by the computation $\oint (z - a)^{-n} dz = 0$ for $n \ge 2$ and Lemma 5 for $n = 1$ . That term contributes $2\pi i \operatorname{Res}_{a_j} f$ .

∎

The same proof works for any simple closed contour on which Cauchy's theorem is available (for example a semicircle, using its convexity and Theorem 4 on a slightly larger convex region). We use a semicircle now.

Example— Two real integrals by residues

(a) $\int_{-\infty}^\infty \frac{dx}{1 + x^2} = \pi$ . Let $\Gamma_R$ be the segment $[-R, R]$ followed by the upper semicircle $C_R$ of radius $R > 1$ . Inside lies one simple pole of $\frac{1}{1 + z^2}$ , at $i$ , with residue $\frac{1}{2i}$ . So $\oint_{\Gamma_R} \frac{dz}{1 + z^2} = 2\pi i \cdot \frac{1}{2i} = \pi$ . On $C_R$ , $|1 + z^2| \ge R^2 - 1$ , so the ML-inequality bounds that part by $\frac{\pi R}{R^2 - 1} \to 0$ . Letting $R \to \infty$ gives $\pi$ .

(b) $\int_{-\infty}^\infty \frac{\cos x}{1 + x^2}\,dx = \frac{\pi}{e}$ . Use $f(z) = \frac{e^{iz}}{1 + z^2}$ instead. On the upper half-plane $|e^{iz}| = e^{-\operatorname{Im} z} \le 1$ , so the same estimate kills $C_R$ . The residue at $i$ is $\frac{e^{i \cdot i}}{2i} = \frac{e^{-1}}{2i}$ . Hence $\int_{-\infty}^\infty \frac{e^{ix}}{1 + x^2}\,dx = 2\pi i \cdot \frac{e^{-1}}{2i} = \frac{\pi}{e}$ . Taking real parts gives the result, and the imaginary part, $\int \frac{\sin x}{1 + x^2}\,dx = 0$ , is consistent with the integrand being odd. (Using $\cos z$ directly would fail: $|\cos z|$ grows like $e^{|\operatorname{Im} z|}$ on the semicircle.)

Applied to $f'/f$ , the residue theorem counts zeros. Argument principle: if $f$ is holomorphic on a neighbourhood of $|z - c| \le R$ with no zeros on the circle, then $\frac{1}{2\pi i}\oint \frac{f'(z)}{f(z)}\,dz$ is the number of zeros inside, counted with multiplicity. (At a zero of order $m$ , $f'/f$ has a simple pole with residue $m$ .) Its corollary, Rouché's theorem, says: if $|g| < |f|$ on the circle, then $f$ and $f + g$ have the same number of zeros inside. For example $z^5 - 3z + 1$ has exactly one zero in $|z| < 1$ , since $|z^5 + 1| \le 2 < 3 = |{-3z}|$ there.

Theorem— Proposition 13 (1/z has no holomorphic extension)

There is no entire function $g$ with $g(z) = 1/z$ for all $z \ne 0$ . More generally, $1/z$ has no primitive on $\C \setminus \{0\}$ .

Proof

If $g$ were entire, Cauchy's theorem would give $\oint_{|z|=1} g = 0$ . But $g = 1/z$ on the circle, and $\oint dz/z = 2\pi i$ . A primitive $F$ of $1/z$ on $\C \setminus \{0\}$ would also force $\oint dz/z = 0$ .

∎

The obstruction is exactly that $1/z$ is unbounded near $0$ . Riemann's removable singularity theorem says that a function holomorphic on a punctured disc and bounded near the puncture extends holomorphically to it. (Apply Theorem 7 to $(z - a)^2 f(z)$ , which is complex-differentiable at $a$ with derivative $0$ .)

ExplanationH

Conformal maps

Theorem— Proposition 14 (holomorphic maps preserve angles)

If $f$ is holomorphic near $z_0$ and $f'(z_0) \ne 0$ , then $f$ preserves the oriented angle between any two smooth curves crossing at $z_0$ .

Proof

A curve $\gamma$ with $\gamma(0) = z_0$ and $\gamma'(0) \ne 0$ is mapped to $f \circ \gamma$ , with tangent $(f \circ \gamma)'(0) = f'(z_0)\gamma'(0)$ by the chain rule. Every tangent vector is multiplied by the same non-zero complex number $f'(z_0) = re^{i\theta}$ , which rotates all of them by $\theta$ . So the angle between any two of them is unchanged.

∎

Where $f'(z_0) = 0$ angles are multiplied: $z \mapsto z^2$ doubles every angle at $0$ . The Möbius transformations $z \mapsto \frac{az + b}{cz + d}$ ( $ad - bc \ne 0$ ) are conformal bijections of the Riemann sphere $\C \cup \{\infty\}$ that send circles and lines to circles and lines. For example $z \mapsto \frac{z - i}{z + i}$ maps the upper half-plane onto the unit disc. Riemann mapping theorem (stated, not proved here): every simply connected open set $U \subsetneq \C$ is conformally equivalent to the open unit disc. Riemann stated it in 1851. Rigorous proofs came around 1900–1912 (Osgood, Carathéodory, Koebe), and the standard textbook proof is due to Fejér and Riesz (1922).

Formal mathematicsF

Complex analysis in Lean and Mathlib

Mathlib's complex analysis is extensive. Holomorphic functions are DifferentiableOn ℂ f U, and contour integrals over circles are circleIntegral, written ∮ z in C(c, R), f z. Mathlib proves Cauchy's theorem for rectangles by a version of Green's theorem (not by Goursat subdivision), and deduces from it the disc theorem, Cauchy's integral formula, analyticity, the Cauchy estimates and Liouville's theorem. We name the notion of the lesson:

HolomorphicOnLean 4Formally verified

/-- `HolomorphicOn f U`: `f` is complex-differentiable at every point of `U` (the lesson's
definition, for open `U`). This is just a name for Mathlib's `DifferentiableOn ℂ f U`. -/
abbrev HolomorphicOn (f : ℂ → ℂ) (U : Set ℂ) : Prop :=
  DifferentiableOn ℂ f U