1 Complex Analysis

Lemma 1 Log growth

✓

For \(t{\gt} 1\) we have \(2\log t \le O(\log t)\)

Proof ▶

Uses definition of big \(O(.)\)

Lemma 2 Square log

✓

For \(t\ge 2\) we have \(\log (t^2) = 2\log t\)

Proof ▶

Lemma 3 Double log

✓

For \(t\ge 2\) we have \(\log (2t) \le \log (t^2)\)

Proof ▶

Uses \(2t \le t^2\), and \(\log (t)\) monotonically increasing.

Lemma 4 Log compare

✓

For \(t\ge 2\) we have \(\log (2t) \le 2\log t\)

Proof ▶

Apply Lemmas 2 and 3.

Lemma 5 Exp rule

✓

For any \(n\ge 1\) and \(\alpha ,\beta \in {\mathbb C}\) we have \(n^{\alpha +\beta } = n^\alpha \cdot n^{\beta }\)

Proof ▶

Lemma 6 Real scale

✓

For \(b\in {\mathbb R}\) and \(w\in {\mathbb C}\) we have \(\Re (bw) = b\Re (w)\).

Proof ▶

Lemma 7 Real series

✓

For a convergent series \(v=\sum _{n=1}^\infty v_n\) with \(v_n\in {\mathbb C}\), we have \(\Re (v) = \sum _{n=1}^\infty \Re (v_n)\).

Proof ▶

Lemma 8 Euler’s formula

✓

For \(a\in {\mathbb R}\) we have \(e^{ia} = \cos (a) + i\sin (a)\)

Proof ▶

Lemma 9 Real cosine

✓

For \(a\in {\mathbb R}\) we have \(\Re (e^{ia}) = \cos (a)\)

Proof ▶

Apply Lemma 8.

Lemma 10 Log inverse

✓

For \(n\ge 1\) we have \(n = e^{\log n}\).

Proof ▶

Lemma 11 Cos even

✓

For \(a\in {\mathbb R}\) we have \(\cos (-a) = \cos (a)\)

Proof ▶

Lemma 12 Cos even

✓

For \(n\ge 1\), \(y\in {\mathbb R}\) we have \(\cos (-y\log n) = \cos (y\log n)\)

Proof ▶

Let \(a=y\log n\). Since \(n\ge 1\) we have \(\log n\ge 0\), so \(a\in {\mathbb R}\). Apply Lemma 11 with \(a=y\log n\).

Lemma 13 Exp form

✓

For \(n\ge 1\) and \(y\in {\mathbb R}\) we have \(n^{-iy} = e^{-iy\log n}\).

Proof ▶

By Lemma 10 \(n^{-iy} = (e^{\log n})^{-iy}\). Then \((e^{\log n})^{-iy} = e^{-iy\log n}\) so \(n^{-iy} = e^{-iy\log n}\).

Lemma 14 Real cosine

✓

For \(n\ge 1\) and \(y\in {\mathbb R}\) we have \(\Re (e^{-iy\log n}) = \cos (-y\log n)\).

Proof ▶

Let \(a=-y\log n\) so \(e^a = e^{-iy\log n}\). Apply Lemma 9 with \(a=-y\log n\).

Lemma 15 Real cosine

✓

For \(n\ge 1\) and \(y\in {\mathbb R}\) we have \(\Re (n^{-iy}) = \cos (-y\log n)\).

Proof ▶

Apply Lemmas 13 and 14.

Lemma 16 Real cosine

✓

For \(n\ge 1\) and \(y\in {\mathbb R}\) we have \(\Re (n^{-iy}) = \cos (y\log n)\).

Proof ▶

Apply Lemmas 12 and 15.

Lemma 17 Double angle

✓

For any \(\theta \in {\mathbb R}\) we have \(\cos (2\theta ) = 2\cos (\theta )^2 - 1\).

Proof ▶

Lemma 18 Cos square

✓

For any \(\theta \in {\mathbb R}\) we have \(2\cos (\theta )^2 = 1+\cos (2\theta )\).

Proof ▶

Apply Lemma 17

Lemma 19 Square expand

✓

For any \(\theta \in {\mathbb R}\) we have \(2(1+\cos (\theta ))^2 = 2 + 4\cos (\theta ) + 2\cos (\theta )^2\).

Proof ▶

We calculate \(2(1+\cos (\theta ))^2 = 2(1 + 2\cos (\theta ) + \cos (\theta )^2) = 2 + 4\cos (\theta ) + 2\cos (\theta )^2.\)

Lemma 20 Trig identity

✓

For any \(\theta \in {\mathbb R}\) we have \(2(1+\cos (\theta ))^2 = 3+4\cos (\theta )+\cos (2\theta )\).

Proof ▶

Apply Lemmas 18 and 19.

Lemma 21 Square nonneg

✓

For \(y\in {\mathbb R}\) we have \(0\le y^2\).

Proof ▶

Lemma 22 Double square

✓

For \(y\in {\mathbb R}\) we have \(0\le 2y^2\).

Proof ▶

Apply Lemma 21.

Lemma 23 Cos square

✓

For any \(\theta \in {\mathbb R}\) we have \(0\le 2(1+\cos (\theta ))^2\).

Proof ▶

Apply Lemma 22 with \(y=1+\cos (\theta )\).

Lemma 24 Trig positive

✓

For any \(\theta \in {\mathbb R}\) we have \(0\le 3+4\cos (\theta )+\cos (2\theta )\).

Proof ▶

Apply Lemmas 20 and 23.

Lemma 25 Trig positive

✓

For \(n\ge 1\) and \(t\in {\mathbb R}\) we have \(0\le 3+4\cos (t\log n)+\cos (2t\log n)\).

Proof ▶

Apply Lemma 24 with \(\theta =t\log n\).

Lemma 26 Series positive

✓

For a convergent series \(r=\sum _{n=1}^\infty r_n\), if \(r_n\ge 0\) for all \(n\ge 1\), then \(r\ge 0\).

Proof ▶

Lemma 27 Real part diff

✓

For any \(w \in {\mathbb C}\), \(\Re (2M-w) = 2M - \Re (w)\).

Proof ▶

Lemma 28 Real part 2M

✓

We have \(\Re (2M-f(z)) = 2M - \Re (f(z))\).

Proof ▶

Apply Lemma 27 with \(w=f(z)\).

Lemma 29 Inequality reversal

✓

For \(x, M\in {\mathbb R}\), if \(x \le M\) then \(2M-x \ge M\).

Proof ▶

Lemma 30 Real part lower bound

✓

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(2M-\Re (w) \ge M\).

Proof ▶

Apply Lemma 29 with \(x=\Re (w)\).

Lemma 31 Real part bound

✓

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(\Re (2M - w) \ge M\).

Proof ▶

Apply Lemmas 28 and 30.

Lemma 32 Real part >0

✓

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(\Re (2M - w) {\gt} 0\).

Proof ▶

Apply Lemmas 28 and 30 with \(w=f(z)\).

Lemma 33 Pos real nonzero

✓

If \(w \in {\mathbb C}\) has \(\Re (w) {\gt} 0\), then \(w \neq 0\).

Proof ▶

Lemma 34 2M minus nonzero

✓

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(2M - w\neq 0\).

Proof ▶

Apply Lemmas 32 and 33.

Lemma 35 Absolute value positive

✓

Let \(z\in {\mathbb C}\). If \(z\neq 0\) then \(|z|{\gt}0\).

Proof ▶

Lemma 36 2M minus mod

✓

For \(w\in {\mathbb C}\) and \(M{\gt}0\), if \(\Re (w) \le M\) then \(|2M - w|{\gt}0\).

Proof ▶

Apply Lemmas 34 and 35 with \(z=2M-w\).

Lemma 37 Real imaginary

✓

For any \(w \in {\mathbb C}\), we have \(w=\Re (w) + i\Im w\).

Proof ▶

Lemma 38 Mod square

✓

For any \(a,b \in {\mathbb R}\), we have \(|a + ib|^2 = a^2 + b^2\).

Proof ▶

Lemma 39 Shifted mod

✓

For any \(a,b,c \in {\mathbb R}\), we have \(|c-a - ib|^2 = (c-a)^2 + b^2\).

Proof ▶

Lemma 40 Mod diff

✓

For any \(a,b,c \in {\mathbb R}\), we have \(|c-a - ib|^2 - |a + ib|^2 = (c-a)^2 - a^2\).

Proof ▶

Apply Lemmas 39 and 38.

Lemma 41 Square expand

✓

For any \(a,c \in {\mathbb R}\), we have \((c-a)^2 = a^2-2ac+c^2\).

Proof ▶

Lemma 42 Square diff

✓

For any \(a,c \in {\mathbb R}\), we have \((c-a)^2 - a^2 = 2c(c-a)\).

Proof ▶

Apply Lemma 41

Lemma 43 Mod diff

✓

For any \(a,b,c \in {\mathbb R}\), we have \(|c-a - ib|^2 - |a + ib|^2 = 2c(c-a)\).

Proof ▶

Apply Lemmas 40 and 42.

Lemma 44 Modulus diff

✓

For any \(w \in {\mathbb C}\), \(|2M-\Re (w) - i\Im w|^2 - |\Re (w) + i\Im w|^2 = 4M(M - \Re (w))\).

Proof ▶

Apply Lemma 43 with \(a=\Re (w)\) and \(b=\Im w\) and \(c=2M\).

Lemma 45 Modulus identity

✓

For any \(w \in {\mathbb C}\), \(|2M-w|^2 - |w|^2 = 4M(M - \Re (w))\).

Proof ▶

Apply Lemmas 44 and 37

Lemma 46 Nonneg product

✓

If \(M{\gt}0\) and \(x \le M\), then \(4M(M-x) \ge 0\).

Proof ▶

Lemma 47 Nonneg product

✓

Let \(M{\gt}0\) and \(w\in {\mathbb C}\). If \(\Re (w) \le M\) then \(4M(M-\Re (w)) \ge 0\).

Proof ▶

Apply Lemma 46 with \(x=\Re (w)\).

Lemma 48 Modulus compare

✓

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(|2M-w|^2 - |w|^2 \ge 0\).

Proof ▶

Apply Lemmas 45 and 47

Lemma 49 Modulus bound

✓

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(|2M-w|^2 \ge |w|^2\).

Proof ▶

Apply Lemma 48.

Lemma 50 Modulus bound

✓

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(|2M-w| \ge |w|\).

Proof ▶

Apply Lemma 49 and take non-negative square-root.

Lemma 51 Modulus order

✓

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(|w|\le |2M-w|\).

Proof ▶

Apply Lemma 50.

Lemma 52 Divide inequality

✓

If \(c{\gt}0\) and \(0\le a\le b\), then \(a/c\le b/c\).

Proof ▶

Lemma 53 Ratio bound

✓

If \(b{\gt}0\) and \(0\le a\le b\), then \(a/b\le 1\).

Proof ▶

Apply Lemma 52 with \(c=b{\gt}0\).

Lemma 54 Ratio bound

✓

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(|2M-w|{\gt}0\) and \(|w|\le |2M-w|\) then \(\frac{|w|}{|2M-w|} \le 1\).

Proof ▶

Apply Lemmas 36 and 51 and 53 with \(a=|w|\) and \(b=|2M-w|\).

Lemma 55 Ratio bound

✓

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) and \(|w|\le |2M-w|\) then \(\frac{|w|}{|2M-w|} \le 1\).

Proof ▶

Apply Lemmas 36 and 54.

Lemma 56 Ratio bound

✓

Let \(M{\gt}0\) and \(w \in {\mathbb C}\). If \(\Re (w) \le M\) then \(\frac{|w|}{|2M-w|} \le 1\).

Proof ▶

Apply Lemmas 51 and 55.

Lemma 57 Triangle inequality

✓

Let \(N,G\in {\mathbb C}\). We have \(|N + G| \le |N| + |G|\)

Proof ▶

Lemma 58 Triangle minus

✓

Let \(N,F\in {\mathbb C}\). We have \(|N - F| \le |N| + |F|\)

Proof ▶

Apply Lemma 57 with \(G=-F\).

Lemma 59 Scaled triangle

✓

Let \(r{\gt}0\) and \(N,F\in {\mathbb C}\). We have \(r|N - F| \le r(|N| + |F|)\)

Proof ▶

Apply Lemmas 57 and 52 with \(a=|N-F|\) and \(b=(|N| + |F|)\).

Lemma 60 Scaled triangle

✓

Let \(r{\gt}0\) and \(N,F\in {\mathbb C}\). We have \(r|N - F| \le r|N| + r|F|\)

Proof ▶

Apply Lemma 59

Lemma 61 Ineq step

✓

Let \(0{\lt}r{\lt}R\) and \(N,F\in {\mathbb C}\). If \(R|F| \le r|N-F|\) then \(R|F| \le r|N| + r|F|\)

Proof ▶

Apply assumption \(R|F| \le r|N-F|\) and Lemma 60

Lemma 62 Rearranged bound

✓

Let \(0{\lt}r{\lt}R\) and \(N,F\in {\mathbb C}\). If \(R|F| \le r|N-F|\) then \((R-r)|F| \le r|N|\)

Proof ▶

Apply Lemma 61

Lemma 63 Abs positive

✓

For \(a\in {\mathbb R}\), if \(a{\gt}0\) then \(|a|=a\).

Proof ▶

Lemma 64 Double positive

✓

For \(a\in {\mathbb R}\), if \(a{\gt}0\) then \(2a{\gt}0\).

Proof ▶

Lemma 65 Scaled abs

✓

For \(a\in {\mathbb R}\), if \(a{\gt}0\) then \(|2a|=2a\).

Proof ▶

Apply Lemmas 63 and 64

Lemma 66 Key bound

✓

Let \(0{\lt}r{\lt}R\), \(M{\gt}0\), and \(F\in {\mathbb C}\). If \(RF \le r|2M-F|\) then \((R-r)|F| \le 2Mr\)

Proof ▶

Apply Lemma 62 with \(N=2M\), and Lemma 65 with \(a=M\).

Lemma 67 Nonneg factor

✓

Let \(0{\lt}r{\lt}R\) and \(F\in {\mathbb C}\). Then we have \((R-r)|F| \ge 0\)

Proof ▶

Lemma 68 Divide bound

✓

Let \(0{\lt}r{\lt}R\), \(M{\gt}0\), and \(F\in {\mathbb C}\). If \((R-r)|F| \le 2Mr\) then \(|F| \le \frac{2Mr}{R-r}\).

Proof ▶

Apply Lemma 52 with \(c=(R-r){\gt}0\) and \(a=(R-r)|F|\) and \(b=2Mr\). Lemma 67 gives \(a\ge 0\).

Lemma 69 Final bound

✓

Let \(0{\lt}r{\lt}R\), \(M{\gt}0\), and \(F\in {\mathbb C}\). If \(R|F| \le r|2M-F|\) then \(|F| \le \frac{2Mr}{R-r}\)

Proof ▶

Apply Lemmas 66 and 68.

Lemma 70 Order nonzero

✓

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic, and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(f(0)=0\) then \(n_0 \neq 0\).

Proof ▶

Lemma 71 Order natural

✓

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic, and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(f\neq 0\) then \(n_0 \in {\mathbb N}\).

Proof ▶

Lemma 72 Factor power

✓

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic at \(0\), and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(n_0\in {\mathbb N}\) then there exists a nhd \(N\) of \(0\) and \(g:{\mathbb C}\to {\mathbb C}\) such that \(g\) is analytic at \(0\), and \(f(z) = z^{n_0} g(z)\) on \(N\).

Proof ▶

Lemma 73 Factor linear

✓

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic at \(0\), and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(n_0\in {\mathbb N}\) and \(n_0\neq 0\), then there exists a nhd \(N\) of \(0\) and \(h:{\mathbb C}\to {\mathbb C}\) such that \(h\) is analytic at \(0\), and \(f(z) = zh(z)\) on \(N\).

Proof ▶

Apply Lemma 72 and let \(h(z)=z^{n_0-1} g(z)\).

Lemma 74 Divide zero

✓

Let \(f:{\mathbb C}\to {\mathbb C}\) be analytic at \(0\), and let \(n_0\) be the analyticOrderAt for \(f\) at \(0\). If \(f\neq 0\) and \(f(0)=0\), then \(h(z)=f(z)/z\) is analytic at \(0\).

Proof ▶

Apply Lemmas 71 and 73 and 70

Lemma 75 Inverse analytic

✓

The function \(f_1(z) = \frac{1}{z}\) is analytic on \(\{ z\in {\mathbb C}: z \neq 0\} \).

Proof ▶

Lemma 76 Analytic mono

✓

Let \(T\subset S\subset {\mathbb C}\) and \(f:S\to {\mathbb C}\). If \(f\) is analytic on \(S\) then \(f\) is analytic on \(T\).

Proof ▶

Lemma 77 Nonzero subset

✓

Let \(0{\lt}R{\lt}1\) and \(V=\{ z\in \overline{{\mathbb D}}_R: z \neq 0\} \) and \(U=\{ z\in {\mathbb C}: z \neq 0\} \). Then \(V\subset U\).

Proof ▶

unfold definitions, using \(\overline{{\mathbb D}}_R\subset {\mathbb C}\).

Lemma 78 Inverse analytic

✓

The function \(f_1(z) = \frac{1}{z}\) is analytic on \(T=\{ z\in \overline{{\mathbb D}}_R: z \neq 0\} \).

Proof ▶

Apply Lemmas 77 and 75 and 76 with \(S=\{ z\in {\mathbb C}: z \neq 0\} \) and \(T=\{ z\in \overline{{\mathbb D}}_R: z \neq 0\} \).

Lemma 79 Product analytic

✓

Let \(T\subset S\subset {\mathbb C}\), and let \(f_1:S\to {\mathbb C}\) and \(f_2:S\to {\mathbb C}\). If \(f_1\) is analytic on \(T\) and \(f_2\) is analytic on \(T\), then \(f_1\cdot f_2\) is analytic on \(T\).

Proof ▶

Lemma 80 Product analytic

✓

Let \(T\subset S\subset {\mathbb C}\), and let \(f_1:S\to {\mathbb C}\) and \(f_2:S\to {\mathbb C}\). If \(f_1\) is analytic on \(T\) and \(f_2\) is analytic on \(S\), then \(f_1\cdot f_2\) is analytic on \(T\).

Proof ▶

Apply Lemmas 79 and 76 with \(f=f_2\)

Lemma 81 Product analytic

✓

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \) and \(f_1:{\mathbb C}\to {\mathbb C}\) and \(f_2:{\mathbb C}\to {\mathbb C}\). If \(f_1\) is analytic on \(T\) and \(f_2\) is analytic on \(\overline{{\mathbb D}}_R\), then \(f_1\cdot f_2\) is analytic on \(T\).

Proof ▶

Apply Lemmas 80 with \(S=\overline{{\mathbb D}}_R\) and \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \).

Lemma 82 Quotient analytic

✓

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \) and \(f:{\mathbb C}\to {\mathbb C}\). If \(f(z)\) is analytic on \(\overline{{\mathbb D}}_R\), then \(f(z)/z\) is analytic on \(T\).

Proof ▶

Apply Lemmas 78 and 81 with \(f_1(z) = 1/z\) and \(f_2(z)=f(z)\).

Lemma 83 On implies within

✓

Let \(V\subset {\mathbb C}\) and \(h:{\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticOn \(V\), then \(h\) is AnalyticWithinAt \(z\) for all \(z\in V\).

Proof ▶

Lemma 84 Within implies on

✓

Let \(h:{\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticWithinAt \(z\) for all \(z\in \overline{{\mathbb D}}_R\), then \(h\) is AnalyticOn \(\overline{{\mathbb D}}_R\).

Proof ▶

Lemma 85 Disk split

✓

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \). Then \(\overline{{\mathbb D}}_R = \{ 0\} \cup T\).

Proof ▶

Unfold definition of \(T\).

Lemma 86 Within union

✓

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \) and \(h: {\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticWithinAt \(0\) and \(h\) is AnalyticWithinAt \(z\) for all \(z\in T\), then \(h\) is AnalyticWithinAt \(z\) for all \(z\in \overline{{\mathbb D}}_R\).

Proof ▶

Apply Lemma 85.

Lemma 87 Within gives on

✓

Proof ▶

Apply Lemmas 84 and 86

Lemma 88 At to within

✓

Let \(h:{\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticAt \(0\), then \(h\) is AnalyticWithinAt \(0\).

Proof ▶

Lemma 89 Local to global

✓

Let \(T=\{ z\in \ \overline{{\mathbb D}}_R : z\neq 0\} \) and \(h: {\mathbb C}\to {\mathbb C}\). If \(h\) is AnalyticAt \(0\) and \(h\) is AnalyticOn \(T\), then \(h\) is AnalyticOn \(\overline{{\mathbb D}}_R\).

Proof ▶

Apply Lemmas 88 and 87.

1.1 Borel-Carathéodory I

Definition 90 Open disk

✓

For \(R{\gt}0\), define the open ball \({\mathbb D}_R := \{ z\in {\mathbb C}: |z| {\lt} R\} \).

Lemma 91 Disk closure

✓

For \(R{\gt}0\), the closure of \({\mathbb D}_R\) equals \(\overline{{\mathbb D}}_R := \{ z\in {\mathbb C}: |z|\le R\} \)

Proof ▶

Lemma 92 In disk bound

✓

For \(R{\gt}0\), if \(w\in \overline{{\mathbb D}}_R\) then \(|w|\le R\).

Proof ▶

Apply Lemma 91.

Lemma 93 Outside disk bound

✓

For \(R{\gt}0\), if \(w\notin {\mathbb D}_R\) then \(|w| \ge R\).

Proof ▶

Apply definition 90.

Lemma 94 Modulus equal

✓

For \(R{\gt}0\), if \(|w|\le R\) and \(|w|\ge R\) then \(|w|=R\).

Proof ▶

Lemma 95 Boundary modulus

✓

For \(R{\gt}0\), if \(w\in \overline{{\mathbb D}}_R\) and \(w\notin {\mathbb D}_R\), then \(|w|=R\).

Proof ▶

Apply Lemmas 92 and 93 and 94.

Lemma 96 Positive modulus

✓

For \(R{\gt}0\) we have \(|R|=R\).

Proof ▶

Lemma 97 Modulus bound

✓

For \(R{\gt}0\) we have \(|R|\le R\).

Proof ▶

Apply Lemma 96 and \(R\le R\).

Lemma 98 Positive radius belongs to its closed disk

✓

For \(R{\gt}0\) we have \(R\in \overline{{\mathbb D}}_R\).

Proof ▶

Apply Lemma 97 and definition 90

Lemma 99 Compactness

✓

For \(R{\gt}0\) the ball \(\overline{{\mathbb D}}_R\) is a compact subset of \({\mathbb C}\).

Proof ▶

Lemma 100 ExtrValThm

✓

If \(K\subset {\mathbb C}\) is compact and \(g:K \to {\mathbb C}\) is continuous, then there exists \(v\in K\) such that \(|g(v)| \ge |g(z)|\) for all \(z\in K\).

Proof ▶

Lemma 101 Disk Boundary

✓

If \(g:\overline{{\mathbb D}}_R \to {\mathbb C}\) is continuous, then there exists \(v\in \overline{{\mathbb D}}_R\) such that \(|g(v)| \ge |g(z)|\) for all \(z\in \overline{{\mathbb D}}_R\).

Proof ▶

Apply Lemmas 99 and 100 with \(K=\overline{{\mathbb D}}_R\).

Lemma 102 Analytic Continuation

✓

If \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) is analytic, then \(h\) is continuous.

Proof ▶

Lemma 103 Max modulus

✓

If \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) is analytic, then there exists \(u\in \overline{{\mathbb D}}_R\) such that \(|h(u)| \ge |h(z)|\) for all \(z\in \overline{{\mathbb D}}_R\).

Proof ▶

Apply Lemmas 101 and 102 with \(g(z)=h(z)\) and \(u=v\).

Lemma 104 Interior max

✓

Let \(R{\gt}0\). Let \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) be analytic. Suppose there exists \(w\in {\mathbb D}_R\) such that \(|h(w)| \ge |h(z)|\) for all \(z\in {\mathbb D}_R\). Then \(|h(z)|=|h(w)|\) for all \(z\in \overline{{\mathbb D}}_R\).

Proof ▶

Apply Lemma 91

Lemma 105 Boundary value

✓

Proof ▶

Apply Lemmas 104 and 98 with \(z=R\).

Lemma 106 Boundary bound

✓

Let \(R{\gt}0\). Let \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) be analytic. Suppose there exists \(w\in {\mathbb D}_R\) such that \(|h(w)| \ge |h(z)|\) for all \(z\in {\mathbb D}_R\). Then \(|h(R)|\ge |h(z)|\) for all \(z\in \overline{{\mathbb D}}_R\)

Proof ▶

Apply Lemmas 104 and 105

Lemma 107 Boundary point

✓

Let \(R{\gt}0\). Let \(h:\overline{{\mathbb D}}_R \to {\mathbb C}\) be analytic. There exists \(v\in \overline{{\mathbb D}}_R\) with \(|v|=R\) such that \(|h(v)|\ge |h(z)|\) for all \(z\in \overline{{\mathbb D}}_R\)

Proof ▶

Apply Lemma 103 to get \(u\in \overline{{\mathbb D}}_R\) such that \(|h(u)|\ge |h(z)|\) for all \(z\in \overline{{\mathbb D}}_R\). If \(u\in {\mathbb D}_R\) then set \(v=R\). Now by Lemma 106 we have \(|v|=|R|=R\). Else \(u\notin {\mathbb D}_R\), then set \(v=u\). Now by Lemma 95 with \(w=u\) we have \(|v|=|u|=R\).

Lemma 108 Boundary point

✓

Let \(R{\gt}0\). Let \(h(z)\) be analytic on \(|z|\le R\). There exists \(v\in {\mathbb C}\) with \(|v|=R\) such that \(|h(v)|\ge |h(z)|\) for all \(z\in {\mathbb C}\) with \(|z|\le R\).

Proof ▶

Apply Lemma 107, and apply Lemma 92 for \(w=v\) and then again for \(w=z\).

Lemma 109 Boundary max

✓

Let \(R{\gt}0\) and \(B\ge 0\). Let \(h(z)\) be a function analytic on \(|z| \le R\). Suppose that \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|= R\). Then there exists \(v\in {\mathbb C}\) with \(|v|=R\) such that \(|h(v)|\ge |h(w)|\) for all \(w\in {\mathbb C}\) with \(|w|\le R\), and \(|h(v)| \le B\).

Proof ▶

Apply Lemma 108, and the assumption \(|h(z)| \le B\) with \(z=v\), since \(|v|=R\).

Lemma 110 Max principle

✓

Let \(R{\gt}0\) and \(B\ge 0\). Let \(h(z)\) be a function analytic on \(|z| \le R\). Suppose that \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|= R\). Then \(|h(w)| \le B\) for all \(w\in {\mathbb C}\) with \(|w|\le R\).

Proof ▶

Apply Lemma 109. By assumption we calculate \(|h(w)|\le |h(v)| \le B\) for all \(w\in {\mathbb C}\) with \(|w|\le R\).

Lemma 111 Easy maximum principle

✓

Let \(R{\gt}0\) and \(B\ge 0\). Let \(h(z)\) be a function analytic on \(|z| \le R\). Suppose that \(|h(w)| \le B\) for all \(w\in {\mathbb C}\) with \(|w|\le R\). Then \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|= R\).

Proof ▶

Take \(z\in {\mathbb C}\) with \(|z|= R\). Then \(|z|\le R\), so by assumption with \(w=z\) we have \(|h(z)| \le B\).

Lemma 112 Maximum modulus principle

✓

Let \(T{\gt}0\) and \(B\ge 0\). Let \(h(z)\) be a function analytic on \(|z| \le T\). We have \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|\le T\) if and only if \(|h(z)| \le B\) for all \(z\in {\mathbb C}\) with \(|z|= T\).

Proof ▶

Apply Lemmas 110 and 111 with \(R=T\).

Lemma 113 Denom nonzero

✓

Let \(R,M{\gt}0\). Suppose \(f(z)\) is an analytic function on \(|z|\le R\) satisfying \(\Re (f(z)) \le M\). Then \(2M - f(z) \neq 0\) for all \(|z|\le R\).

Proof ▶

For each \(z\) with \(|z|\le R\), apply Lemma 34 with \(w=f(z)\).

Lemma 114 Ratio bound

✓

Let \(R,M{\gt}0\). Suppose \(f(z)\) is an analytic function on \(|z|\le R\) satisfying \(\Re (f(z)) \le M\). For any \(z\) with \(|z| \le R\), we have \( \frac{|f(z)|}{|2M - f(z)|}\le 1\).

Proof ▶

For each \(z\) with \(|z|\le R\), apply Lemma 56 with \(w=f(z)\).

Lemma 115 Removable zero

✓

Let \(R{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\). Then the function \(h(z) = f(z)/z\) is analytic on \(|z| \le R\).

Proof ▶

Apply ??.

Lemma 116 Quotient analytic

✓

Let \(R{\gt}0\). If \(h_1(z)\) and \(h_2(z)\) are analytic for \(|z|\le R\) and \(h_2(z)\neq 0\) for all \(|z|\le R\), then \(h_1(z)/h_2(z)\) is analytic for \(|z|\le R\).

Proof ▶

Definition 117 Modified function

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). Define the function \(f_M(z)\) for \(|z| \le R\) as

\[ f_M(z) = \frac{f(z)/z}{2M - f(z)}. \]

Lemma 118 g analytic

✓

The function \(f_M(z)\) from Definition 117 is analytic on \(|z| \le R\).

Proof ▶

Write \(f_M(z) = h_1(z)/h_2(z)\) where \(h_1(z)=f(z)/z\) and \(h_2(z)=2M-f(z)\). Then apply Lemma 116 with \(h_1(z)\) and \(h_2(z)\), using Lemma 115 and Lemma 113.

Lemma 119 Quotient modulus

✓

Let \(a,b\in {\mathbb C}\). If \(b\neq 0\) then \(|a/b| = |a|/|b|\).

Proof ▶

Lemma 120 g modulus

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). We have \(|f_M(z)| = \frac{|f(z)/z|}{|2M - f(z)|}\).

Proof ▶

For each \(|z|\le R\), apply Definition 117, and Lemma 119 with \(a=f(z)/z\) and \(b=2M-f(z)\). Note \(b\neq 0\) by Lemma 113.

Lemma 121 Quotient radius

✓

Let \(T{\gt}0\) and \(z,w\in {\mathbb C}\). If \(|z|=T\) then \(|w/z| = |w|/T\).

Proof ▶

Lemma 122 Boundary g

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(z\in {\mathbb C}\) with \(|z|=R\), we have \(|f_M(z)| = \frac{|f(z)|/R}{|2M - f(z)|}\).

Proof ▶

Apply Lemmas 120 and 121 with \(w=f(z)\) and \(T=R{\gt}0\).

Lemma 123 Scaled ratio

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(z\) with \(|z| \le R\), we have \( \frac{|f(z)|/R}{|2M - f(z)|}\le 1/R\).

Proof ▶

Apply Lemma 114.

Lemma 124 Boundary bound

✓

Proof ▶

Apply Lemmas 122 and 123.

Lemma 125 Interior bound

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(z\in {\mathbb C}\) with \(|z| \le R\), we have \(|f_M(z)| \le 1/R\).

Proof ▶

Apply Lemmas 124 and 112 with \(B=1/R\) and \(T=R\) and \(h(z)=f_M(z)\).

Lemma 126 g at r

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r{\lt}R\) and any \(z\in {\mathbb C}\) with \(|z|=r\), we have \(|f_M(z)| = \frac{|f(z)|/r}{|2M - f(z)|}\).

Proof ▶

Apply Lemmas 120 and 121 with \(w=f(z)\) and \(T=r{\gt}0\).

Lemma 127 g bound r

✓

Proof ▶

Apply Lemmas 125 and 126 with \(|z|=r{\lt}R\).

Lemma 128 Fraction swap

✓

Let \(a,b,r,R{\gt}0\). If \(\frac{a/r}{b} \le 1/R\) then \(Ra \le rb\).

Proof ▶

Lemma 129 Rearranged bound

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R\) and any \(z\in {\mathbb C}\) with \(|z|=r\), we have \(R|f(z)| \le r|2M - f(z)|\).

Proof ▶

Apply Lemmas 127 and 128 with \(a=|f(z)|{\gt}0\) and \(b=|2M - f(z)|{\gt}0\).

Lemma 130 Circle bound

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R\) and any \(z\in {\mathbb C}\) with \(|z|=r\), we have

\[ |f(z)| \le \frac{2r}{R-r}M. \]

Proof ▶

For each \(|z| \le R\), apply Lemmas 129 and 69 with \(F=f(z)\).

Lemma 131 Circle bound

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R\), and any \(z\in {\mathbb C}\) with \(|z|=r\) we have

\[ |f(z)| \le \frac{2r}{R-r}M. \]

Proof ▶

Apply Lemma 130.

Lemma 132 BC bound

✓

\[ |f(z)| \le \frac{2r}{R-r}M. \]

Proof ▶

Apply Lemmas 131 and 112 with \(B=\frac{2r}{R-r}M\) and \(T=r\) and \(h(z)=f(z)\).

Theorem 133 Borel-Carathéodory I

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R,\)

\[ \sup _{|z| \le r} |f(z)| \le \frac{2r}{R-r}M. \]

Proof ▶

Apply Lemma 132 and definition of supremum \(\sup _{|z| \le r}\).

1.2 Borel-Carathéodory II

Lemma 134 Cauchy’s Integral Formula for \(f'\)

✓

Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\) and any \(r'\) with \(0 {\lt} r {\lt} r' {\lt} R\),

\[ f'(z) = \frac{1}{2\pi i} \oint _{|w|=r'} \frac{f(w)}{(w-z)^2}dw. \]

Proof ▶

Lemma 135 Differential of \(w(t)\)

✓

For \(w(t) = r'e^{it}\), we have \(dw = ir'e^{it}dt\).

Proof ▶

Differentiate \(w(t)\) with respect to \(t\).

Lemma 136 CIF for \(f'\), Parameterized

✓

Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\) and any \(r'\) with \(0 {\lt} r {\lt} r' {\lt} R\),

\[ f'(z) = \frac{1}{2\pi i} \int _{0}^{2\pi } \frac{f(r'e^{it})}{(r'e^{it}-z)^2} (ir'e^{it})\, dt. \]

Proof ▶

Apply Lemmas 134 and 135, and unfold definition of the circle integral \(\oint \) over \(w\in C(0,r')\).

Lemma 137 CIF for \(f'\), Simplified

✓

Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\) and any \(r'\) with \(0 {\lt} r {\lt} r' {\lt} R\),

\[ f'(z) = \frac{1}{2\pi } \int _{0}^{2\pi } \frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\, dt. \]

Proof ▶

Apply Lemma 136 and cancel \(i\) from the numerator and denominator.

Lemma 138 Derivative modulus

✓

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(|f'(z)| = \left|\frac{1}{2\pi } \int _{0}^{2\pi } \frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\, dt \right|\).

Proof ▶

Apply modulus to both sides of the equality in Lemma 137.

Lemma 139 Integral bound

✓

For an integrable function \(g(t)\), we have \(|\int _a^b g(t) dt| \le \int _a^b |g(t)| dt\).

Proof ▶

Lemma 140 Modulus of \(f'\)

✓

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(|f'(z)| \le \frac{1}{2\pi } \int _{0}^{2\pi } \left|\frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2} \right| \, dt\).

Proof ▶

Apply Lemmas 138 and 139.

Lemma 141 Integrand modulus

✓

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(|f(r'e^{it}) r'e^{it}| = |f(r'e^{it})| \cdot |r'e^{it}|\).

Proof ▶

Apply modulus property \(|ab|=|a||b|\).

Lemma 142 Modulus one

✓

For \(t\in {\mathbb R}\) we have \(|e^{it}| = e^{\Re (it)}\)

Proof ▶

Lemma 143 Cosine part

✓

For \(t\in {\mathbb R}\) we have \(\Re (it) = 0\)

Proof ▶

Lemma 144 Euler part

✓

For \(t\in {\mathbb R}\) we have \(e^{\Re (it)} =e^0\).

Proof ▶

Apply Lemma 143.

Lemma 145 Exp zero one

✓

We have \(e^0 = 1\).

Proof ▶

Lemma 146 Cosine relation

✓

For \(t\in {\mathbb R}\) we have \(e^{\Re (it)} = 1\)

Proof ▶

Apply Lemmas 144 and 145

Lemma 147 Unit modulus

✓

For \(t\in {\mathbb R}\) we have \(|e^{it}| = 1\)

Proof ▶

Apply Lemmas 142 and 146

Lemma 148 Scaled modulus

✓

For \(a{\gt}0\) and \(t\in {\mathbb R}\) we have \(|ae^{it}| = a\)

Proof ▶

Apply Lemma 147 and calculate \(|ae^{it}| = |a|\cdot |e^{it}| = a\cdot 1 = a\).

Lemma 149 Integrand modulus

✓

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(|f(r'e^{it}) r'e^{it}| = r' |f(r'e^{it})|\).

Proof ▶

Apply Lemmas 141 and 148 with \(a=r'\).

Lemma 150 Square modulus

✓

For any \(c \in {\mathbb C}\), \(|c^2| = |c|^2\).

Proof ▶

Lemma 151 Shifted modulus

✓

For any \(w,z \in {\mathbb C}\), \(|(w-z)^2| = |w-z|^2\).

Proof ▶

Apply Lemma 150 with \(c=w-z\).

Lemma 152 Reverse triangle

✓

For any \(w, z\in {\mathbb C}\), we have \(|w|-|z| \le |w-z|\).

Proof ▶

Lemma 153 Reverse triangle

✓

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\), we have \(|r'e^{it}|-|z| \le |r'e^{it}-z|\).

Proof ▶

Apply Lemma 152 with \(w=r'e^{it}\).

Lemma 154 Reverse triangle

✓

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\), we have \(r' -|z| \le |r'e^{it}-z|\).

Proof ▶

Apply Lemmas 153 and 148 with \(a=r'\)

Lemma 155 Radius relation

✓

Let \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) with \(|z|\le r\). Then \(0{\lt}r' - |z|\).

Proof ▶

We calculate \(|z| \le r {\lt} r'\) by assumption, so \(0 {\lt} r' - |z|\).

Lemma 156 Radius relation

✓

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) and \(z\in {\mathbb C}\) with \(|z|\le r\). Then \(r' - r \le |r'e^{it}-z|\).

Proof ▶

Apply Lemma 154 and \(|z|\le r\).

Lemma 157 Radius relation

✓

If \(0{\lt}r{\lt}r'\) then \(r'-r{\gt}0\)

Proof ▶

Calculation

Lemma 158 Radius relation

✓

If \(0{\lt}r{\lt}r'\) then \((r'-r)^2{\gt}0\)

Proof ▶

Apply Lemma 157

Lemma 159 Radius relation

✓

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\)and \(z\in {\mathbb C}\) with \(|z|\le r\). Then \((r' - r)^2 \le |r'e^{it}-z|^2\).

Proof ▶

Apply Lemmas 156 and 158.

Lemma 160 Radius relation

✓

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\)and \(z\in {\mathbb C}\) with \(|z|\le r\). Then \(|(r'e^{it}-z)^2| = |r'e^{it}-z|^2\).

Proof ▶

Apply Lemmas 156 and 158.

Lemma 161 Reverse triangle

✓

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) with \(|z|\le r\), we have \(0 {\lt} |r'e^{it}-z|\).

Proof ▶

Apply Lemmas 154 and 155.

Lemma 162 Positive nonzero

✓

For \(w\in {\mathbb C}\), if \(|w|{\gt}0\) then \(w\neq 0\).

Proof ▶

Lemma 163 Reverse triangle

✓

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) with \(|z|\le r\), we have \(r'e^{it}-z \neq 0\).

Proof ▶

Apply Lemmas 161 and 162 with \(w=r'e^{it}-z\).

Lemma 164 Reverse triangle

✓

Let \(t\in {\mathbb R}\) and \(0 {\lt} r {\lt} r' {\lt} R\) and \(z\in {\mathbb C}\) with \(|z|\le r\), we have \((r'e^{it}-z)^2 \neq 0\).

Proof ▶

Apply Lemma 163, and Mathlib mul_self_ne_zero

Lemma 165 Division bound

✓

If \(a,b\in {\mathbb C}\) and \(b\neq 0\) then \(|a/b|=|a|/|b|\).

Proof ▶

Lemma 166 Integrand modulus

✓

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(\left|\frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\right| = \frac{|f(r'e^{it}) r'e^{it}|}{|(r'e^{it}-z)^2|}\).

Proof ▶

Apply Lemma 165 with \(a=f(r'e^{it}) r'e^{it}\) and \(b=(r'e^{it}-z)^2\). Here \(b\neq 0\) by Lemma 164.

Lemma 167 Product modulus

✓

Proof ▶

Apply Lemmas 166 and 149.

Lemma 168 Product modulus

✓

Proof ▶

Apply Lemmas 167 and 160.

Lemma 169 Product modulus

✓

Let \(0 {\lt} r {\lt} r' {\lt} R\). Let \(f\) be analytic on \(|z| \le R\). For any \(z\) with \(|z| \le r\), we have \(\frac{r'|f(r'e^{it})|}{|r'e^{it}-z|^2} \le \frac{r'|f(r'e^{it})|}{(r'-r)^2}\).

Proof ▶

Apply Lemmas 168 and 159.

Lemma 170 Product modulus

✓

Proof ▶

Apply Lemmas 168 and 169.

Lemma 171 Point bound

✓

Let \(M,R{\gt}0\) and \(0{\lt}r'{\lt}R\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(t \in {\mathbb R}\) we have \(|f(r'e^{it})| \le \frac{2r' M}{R-r'}\).

Proof ▶

Note \(w=r'e^{it}\) satisfies \(|w|=r'{\lt}R\) by Lemma 148 with \(a=r'\). Then apply Lemma 132.

Lemma 172 Integrand bound

✓

Let \(M,R{\gt}0\) and \(0{\lt}r{\lt}r'{\lt}R\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(t \in {\mathbb R}\) we have \(\left|\frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\right| \le \frac{2(r')^2M}{(R-r')(r'-r)^2}\).

Proof ▶

Apply Lemmas 170 and 171.

Lemma 173 Integral inequality

✓

If \(g(t) \le C\) for all \(t \in [a,b]\), then \(\int _a^b g(t) dt \le \int _a^b C dt\).

Proof ▶

Lemma 174 Derivative bound

✓

Let \(M,R{\gt}0\) and \(0{\lt}r{\lt}r'{\lt}R\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(t \in {\mathbb R}\) we have \(|f'(z)| \le \frac{1}{2\pi } \int _{0}^{2\pi } \frac{2(r')^2M}{(R-r')(r'-r)^2} dt\).

Proof ▶

Apply Lemmas 140, 172 and 173 with \(g(t)=\left|\frac{f(r'e^{it}) r'e^{it}}{(r'e^{it}-z)^2}\right|\) and \(C=\frac{2(r')^2M}{(R-r')(r'-r)^2}\)

Lemma 175 Integrate one

✓

We have \(\int _0^{2\pi } dt = 2\pi \).

Proof ▶

Lemma 176 Exponential integral

✓

We have \(\frac{1}{2\pi }\int _0^{2\pi } dt = 1\).

Proof ▶

Apply Lemma 175 and simplify.

Lemma 177 Derivative bound

✓

Let \(M,R{\gt}0\) and \(0{\lt}r{\lt}r'{\lt}R\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). Then we have \(|f'(z)| \le \frac{2(r')^2M}{(R-r')(r'-r)^2}\).

Proof ▶

Apply Lemmas 174 and 176.

Lemma 178 Radius compare

✓

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(r {\lt} r'\).

Proof ▶

Since \(r{\lt}R\), we have \(2r {\lt} r+R\). Dividing by 2 gives \(r {\lt} (r+R)/2\).

Lemma 179 Radius compare

✓

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(r' {\lt} R\).

Proof ▶

Since \(r{\lt}R\), we have \(r+R {\lt} 2R\). Dividing by 2 gives \((r+R)/2 {\lt} R\).

Lemma 180 Intermediate radius

✓

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(r {\lt} r' {\lt} R\).

Proof ▶

Apply Lemmas 178 and 179.

Lemma 181 Radius formula

✓

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(R-r' = \frac{R-r}{2}\).

Proof ▶

We calculate \(R - \frac{r+R}{2} = \frac{2R - (r+R)}{2} = \frac{R-r}{2}\).

Lemma 182 Radius formula

✓

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(r'-r = \frac{R-r}{2}\).

Proof ▶

We calculate \(\frac{r+R}{2} - r = \frac{r+R - 2r}{2} = \frac{R-r}{2}\).

Lemma 183 Denominator form

✓

Given \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \((R-r')(r'-r)^2 = \frac{(R-r)^3}{8}\).

Proof ▶

Apply Lemmas 181 and 182 and calculate \(\left(\frac{R-r}{2}\right) \cdot \left(\frac{R-r}{2}\right)^2 = \frac{(R-r)}{2}\frac{(R-r)^2}{4} = \frac{(R-r)^3}{8}\).

Lemma 184 Numerator form

✓

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(2(r')^2M = \frac{(R+r)^2 M}{2}\).

Proof ▶

We calculate \(2(r')^2M = 2\left(\frac{R+r}{2}\right)^2M = 2\frac{(R+r)^2}{4}M =\frac{(R+r)^2 M}{2}\)

Lemma 185 Fraction simplify

✓

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(\frac{2(r')^2M}{(R-r')(r'-r)^2} = \frac{(R+r)^2 M/2}{(R-r)^3/8}\).

Proof ▶

Apply Lemmas 184 and 183.

Lemma 186 Fraction simplify

✓

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\), we have \(\frac{(R+r)^2 M/2}{(R-r)^3/8} = \frac{4(R+r)^2 M}{(R-r)^3}\).

Proof ▶

Simplify fraction

Lemma 187 Fraction simplify

✓

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(\frac{2(r')^2M}{(R-r')(r'-r)^2} = \frac{4(R+r)^2 M}{(R-r)^3}\).

Proof ▶

Apply Lemmas 185 and 186.

Lemma 188 Inequality fact

✓

Given \(r {\lt} R\), we have \(R+r {\lt} 2R\).

Proof ▶

calculation

Lemma 189 Sum positive

✓

Given \(0 {\lt} r {\lt} R\), we have \(0 {\lt} R+r\).

Proof ▶

Lemma 190 Double positive

✓

Given \(0 {\lt} R\), we have \(2R {\gt} 0\).

Proof ▶

Lemma 191 Square fact

✓

If \(0 {\lt} a {\lt} b\), then \(a^2 {\lt} b^2\).

Proof ▶

Lemma 192 Square bound

✓

Given e, we have \((R+r)^2 {\lt} (2R)^2\).

Proof ▶

Let \(a = R+r\) and \(b = 2R\). From Lemma 189, \(a{\gt}0\). From Lemma 190, \(b{\gt}0\). From Lemma 188, \(a{\lt}b\). Apply Lemma 191.

Lemma 193 Square identity

✓

For any \(R{\gt}0\), we have \((2R)^2 = 4R^2\).

Proof ▶

We calculate \((2R)^2 = 2^2 R^2 = 4R^2\).

Lemma 194 Square bound

✓

Given \(0 {\lt} r {\lt} R\), we have \((R+r)^2 {\lt} 4R^2\).

Proof ▶

Apply Lemmas 192 and 193.

Lemma 195 Square bound

✓

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\), we have \(4(R+r)^2M {\lt} 16R^2M\).

Proof ▶

Apply Lemma 194 and multiply by \(4M{\gt}0\).

Lemma 196 Bound simplify

✓

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\), we have \(\frac{4(R+r)^2 M}{(R-r)^3} {\lt} \frac{16R^2 M}{(R-r)^3}\).

Proof ▶

Apply Lemma 195 to the numerator of the fraction.

Lemma 197 Fraction simplify

✓

Given \(M{\gt}0\) and \(0 {\lt} r {\lt} R\) with \(r'=\frac{r+R}{2}\), we have \(\frac{2(r')^2M}{(R-r')(r'-r)^2} \leq \frac{16R^2 M}{(R-r)^3}\).

Proof ▶

Apply Lemmas 187 and 196.

Theorem 198 Borel-Carathéodory II

✓

Let \(R,M{\gt}0\). Let \(f\) be analytic on \(|z| \le R\) such that \(f(0)=0\) and suppose \(\Re f(z) \le M\) for all \(|z| \le R\). For any \(0{\lt}r {\lt} R\) and any \(|z|\le r\),

\[ |f'(z)| \le \frac{16M R^2}{(R-r)^3}. \]

Proof ▶

Apply Lemmas 197 and 177 with \(r'=\frac{r+R}{2}\).

1.3 Integral Antiderivative

Lemma 199 Cauchy rectangles

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Then for any \(z, w \in \overline{{\mathbb D}}_{R}\),

\begin{align*} \left(\int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(x + i\, z.\operatorname {Im}) \, dx\right) & - \left(\int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(x + i\, w.\operatorname {Im}) \, dx\right) \\ & + i \left(\int _{z.\operatorname {Im}}^{w.\operatorname {Im}} f(w.\operatorname {Re}+ i y) \, dy\right) - i \left(\int _{z.\operatorname {Im}}^{w.\operatorname {Im}} f(z.\operatorname {Re}+ i y) \, dy\right) = 0. \end{align*}

Proof ▶

Let the four corners of a rectangle be \(A = z.\operatorname {Re}+ i\, z.\operatorname {Im}\), \(B = w.\operatorname {Re}+ i\, z.\operatorname {Im}\), \(C = w.\operatorname {Re}+ i\, w.\operatorname {Im}\), and \(D = z.\operatorname {Re}+ i\, w.\operatorname {Im}\). Since \(z, w \in \overline{{\mathbb D}}_{R}\), all four corners lie within the closed disk \(\overline{{\mathbb D}}_{R_0}\). The assumption is that \(f\) is analytic on a neighborhood of \(\overline{{\mathbb D}}_{R_0}\). This means there exists an open set \(U\) containing \(\overline{{\mathbb D}}_{R_0}\) on which \(f\) is analytic. The rectangle with corners \(A, B, C, D\) is contained in \(\overline{{\mathbb D}}_{R_0}\), and therefore also in \(U\).

By Cauchy’s Integral Theorem for a rectangle (Mathlib: integral_boundary_rect_eq_zero_of_differentiableOn), the integral of an analytic function over the boundary of the rectangle is zero. We can express this boundary integral as the sum of four path integrals:

\[ \oint _{\partial \text{Rect}} f(\zeta )\, d\zeta = \int _A^B f(\zeta )\, d\zeta + \int _B^C f(\zeta )\, d\zeta + \int _C^D f(\zeta )\, d\zeta + \int _D^A f(\zeta )\, d\zeta = 0. \]

We evaluate each integral:

Path from \(A\) to \(B\): \(\zeta (x) = x + i\, z.\operatorname {Im}\) for \(x\) from \(z.\operatorname {Re}\) to \(w.\operatorname {Re}\). So \(d\zeta = dx\).

\[ \int _A^B f(\zeta )\, d\zeta = \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(x + i\, z.\operatorname {Im}) \, dx. \]
Path from \(B\) to \(C\): \(\zeta (y) = w.\operatorname {Re}+ i\, y\) for \(y\) from \(z.\operatorname {Im}\) to \(w.\operatorname {Im}\). So \(d\zeta = i\, dy\).

\[ \int _B^C f(\zeta )\, d\zeta = i \int _{z.\operatorname {Im}}^{w.\operatorname {Im}} f(w.\operatorname {Re}+ i y) \, dy. \]
Path from \(C\) to \(D\): \(\zeta (x) = x + i\, w.\operatorname {Im}\) for \(x\) from \(w.\operatorname {Re}\) to \(z.\operatorname {Re}\). So \(d\zeta = dx\).

\[ \int _C^D f(\zeta )\, d\zeta = \int _{w.\operatorname {Re}}^{z.\operatorname {Re}} f(x + i\, w.\operatorname {Im}) \, dx = - \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(x + i\, w.\operatorname {Im}) \, dx. \]
Path from \(D\) to \(A\): \(\zeta (y) = z.\operatorname {Re}+ i\, y\) for \(y\) from \(w.\operatorname {Im}\) to \(z.\operatorname {Im}\). So \(d\zeta = i\, dy\).

\[ \int _D^A f(\zeta )\, d\zeta = i \int _{w.\operatorname {Im}}^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i y) \, dy = - i \int _{z.\operatorname {Im}}^{w.\operatorname {Im}} f(z.\operatorname {Re}+ i y) \, dy. \]

Summing these four integrals gives the equation:

\[ \left(\int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(x + i\, z.\operatorname {Im}) \, dx\right) + i \left(\int _{z.\operatorname {Im}}^{w.\operatorname {Im}} f(w.\operatorname {Re}+ i y) \, dy\right) - \left(\int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(x + i\, w.\operatorname {Im}) \, dx\right) - i \left(\int _{z.\operatorname {Im}}^{w.\operatorname {Im}} f(z.\operatorname {Re}+ i y) \, dy\right) = 0. \]

Rearranging the terms to match the statement of the lemma concludes the proof.

Definition 200 Integral along the taxicab path

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Define the function \(I_f:\overline{{\mathbb D}}_R\to \mathbb {C}\) by

\[ I_f(z) := \int _0^{z.\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i\tau )\, d\tau . \]

Lemma 201 Integral form

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\) and \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\). Then

\[ I_f(z+h) = \int _0^{(z+h).\operatorname {Re}} f(t)\, dt + i \int _0^{(z+h).\operatorname {Im}} f((z+h).\operatorname {Re}+ i\tau )\, d\tau . \]

Proof ▶

Apply definition 200 with \(z+h\).

Lemma 202 Integral form

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\). Then

\[ I_f(z) = \int _0^{z.\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i\tau )\, d\tau . \]

Proof ▶

Apply definition 200 with \(z\)

Lemma 203 Integral form

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ I_f(w) = \int _0^{(z+h).\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} f((z+h).\operatorname {Re}+ i\tau )\, d\tau . \]

Proof ▶

Apply definition 200 with \(w\), noting that \(w.\operatorname {Re}= (z+h).\operatorname {Re}\) and \(w.\operatorname {Im}= z.\operatorname {Im}\).

Lemma 204 Difference form

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ I_f(z+h) - I_f(w) = i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f((z+h).\operatorname {Re}+ i\tau )\, d\tau . \]

Proof ▶

Take the difference of lemma 201 and lemma 203, noting the terms involving \(\int f(t)\, dt\) cancel. The remaining terms are combined using properties of integrals.

Lemma 205 Initial form

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ I_f(w) - I_f(z) = \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} [f(w.\operatorname {Re}+ i\tau ) - f(z.\operatorname {Re}+ i\tau )]\, d\tau . \]

Proof ▶

Apply lemma 203 and lemma 202, note that \(w.\operatorname {Im}= z.\operatorname {Im}\), and combine integrals.

Lemma 206 Horizontal strip

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t) dt - \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t + i\, z.\operatorname {Im}) dt + i \int _{0}^{z.\operatorname {Im}} f(w.\operatorname {Re}+ i\tau ) d\tau - i \int _{0}^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i\tau ) d\tau = 0. \]

Proof ▶

Apply lemma 199 with the points \(z' := z.\operatorname {Re}\) and \(w' := (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). The four corners of the rectangle are \(z.\operatorname {Re}\), \((z+h).\operatorname {Re}\), \((z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\), and \(z.\operatorname {Re}+ i\, z.\operatorname {Im}\). Substituting \(z'\) and \(w'\) into the formula from lemma 199 yields the desired identity.

Lemma 207 Rearrangement step

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ i \int _0^{z.\operatorname {Im}} [f(w.\operatorname {Re}+ i\tau ) - f(z.\operatorname {Re}+ i\tau )]\, d\tau = \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt - \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt. \]

Proof ▶

We start with the identity from lemma 206. The assumptions are: \(0{\lt}R{\lt}R_0{\lt}1\), \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analytic on a neighborhood of \(\overline{{\mathbb D}}_{R_0}\), \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) with \(z+h \in \overline{{\mathbb D}}_R\), and \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). The identity is:

By the linearity of integration, we can combine the last two terms:

\[ i \int _{0}^{z.\operatorname {Im}} f(w.\operatorname {Re}+ i\tau ) d\tau - i \int _{0}^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i\tau ) d\tau = i \left( \int _{0}^{z.\operatorname {Im}} f(w.\operatorname {Re}+ i\tau ) d\tau - \int _{0}^{z.\operatorname {Im}} f(z.\operatorname {Re}+ i\tau ) d\tau \right) = i \int _0^{z.\operatorname {Im}} [f(w.\operatorname {Re}+ i\tau ) - f(z.\operatorname {Re}+ i\tau )]\, d\tau . \]

Substituting this back into the identity gives:

\[ \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t) dt - \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t + i\, z.\operatorname {Im}) dt + i \int _0^{z.\operatorname {Im}} [f(w.\operatorname {Re}+ i\tau ) - f(z.\operatorname {Re}+ i\tau )]\, d\tau = 0. \]

To obtain the desired result, we isolate the term involving the integral over \(\tau \) by moving the other two integral terms to the right-hand side of the equation:

This completes the proof.

Lemma 208 Shift integral

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) satisfy \(z+h \in \overline{{\mathbb D}}_R\), and let \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). Then

\[ I_f(w) - I_f(z) = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt. \]

Proof ▶

The assumptions are: \(0{\lt}R{\lt}R_0{\lt}1\), \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analytic on a neighborhood of \(\overline{{\mathbb D}}_{R_0}\), \(z \in \overline{{\mathbb D}}_R\), \(h\in {\mathbb C}\) with \(z+h \in \overline{{\mathbb D}}_R\), and \(w = (z+h).\operatorname {Re}+ i\, z.\operatorname {Im}\). From lemma 205, we have the expression:

\[ I_f(w) - I_f(z) = \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt + i \int _0^{z.\operatorname {Im}} [f(w.\operatorname {Re}+ i\tau ) - f(z.\operatorname {Re}+ i\tau )]\, d\tau . \]

From lemma 207, we have an identity for the second term in the expression above:

We substitute this identity into the expression for \(I_f(w) - I_f(z)\):

\[ I_f(w) - I_f(z) = \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt + \left( \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt - \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt \right). \]

The terms \(\int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt\) and \(-\int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t)\, dt\) cancel each other out.

\[ I_f(w) - I_f(z) = \int _{z.\operatorname {Re}}^{w.\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt. \]

Finally, we use the definition of \(w\), which states \(w.\operatorname {Re}= (z+h).\operatorname {Re}\). Substituting this into the upper limit of the integral gives the final result:

\[ I_f(w) - I_f(z) = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt. \]

Lemma 209 L path

✓

\[ I_f(z+h)-I_f(z) = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(t + i\, z.\operatorname {Im})\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f((z+h).\operatorname {Re}+ i\tau )\, d\tau . \]

Proof ▶

The result follows by summing the identities from lemma 208 and lemma 204, using the identity \(I_f(z+h)-I_f(z) = (I_f(w) - I_f(z)) + (I_f(z+h) - I_f(w))\).

Lemma 210 Add-sub step

✓

\[ I_f(z+h)-I_f(z) = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z) + f(z))\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z) + f(z))\, d\tau . \]

Proof ▶

The identity follows by starting with the expression for \(I_f(z+h)-I_f(z)\) from lemma 209 and adding and subtracting the term \(f(z)\) within each integrand, which is an algebraic identity.

Lemma 211 Linearity split

✓

\begin{align*} I_f(z+h)-I_f(z) = & \left( \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt + \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt \right) \\ & + i \left( \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau + \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau \right). \end{align*}

Proof ▶

We begin with the identity from lemma 210, which holds under the assumptions that \(0{\lt}R{\lt}R_0{\lt}1\), \(f\) is analytic on a neighborhood of \(\overline{{\mathbb D}}_{R_0}\), \(z \in \overline{{\mathbb D}}_R\), and \(h\in {\mathbb C}\) with \(z+h \in \overline{{\mathbb D}}_R\):

We apply the linearity property of the integral, \(\int (g+k) = \int g + \int k\), to each of the two integrals on the right-hand side. For the first integral, we group the integrand as \((f(t + i\, z.\operatorname {Im}) - f(z)) + f(z)\). Applying linearity yields:

\[ \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z) + f(z))\, dt = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt + \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt. \]

For the second integral, we group the integrand as \((f((z+h).\operatorname {Re}+ i\tau ) - f(z)) + f(z)\). Applying linearity yields:

\[ \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z) + f(z))\, d\tau = \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau + \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau . \]

Substituting these expanded forms back into the original equation for \(I_f(z+h)-I_f(z)\), and distributing the factor of \(i\) for the second part, we obtain the desired result:

Lemma 212 Integral of constant over L-path

✓

\[ \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau = f(z) \cdot h. \]

Proof ▶

The left side is the integral of the constant function \(w \mapsto f(z)\) over the L-shaped path. Thus we calculate

\begin{align*} \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau & = f(z) \cdot ((z+h).\operatorname {Re}- z.\operatorname {Re}) + i \cdot f(z) \cdot ((z+h).\operatorname {Im}- z.\operatorname {Im}) \\ & = f(z) \cdot (h.\operatorname {Re}+ i \cdot h.\operatorname {Im}) = f(z) \cdot h. \end{align*}

Lemma 213 Difference decomposition

✓

\[ I_f(z+h)-I_f(z) = h \cdot f(z) + \mathrm{Err}(z,h), \]

where \(\mathrm{Err}(z,h)\) is defined as

\[ \mathrm{Err}(z,h) := \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau . \]

Proof ▶

We start with the expression for \(I_f(z+h)-I_f(z)\) from lemma 211. The assumptions are that \(f\) is analytic on a neighborhood of \(\overline{{\mathbb D}}_{R_0}\), \(z \in \overline{{\mathbb D}}_R\), and \(h \in {\mathbb C}\) such that \(z+h \in \overline{{\mathbb D}}_R\).

\[ I_f(z+h)-I_f(z) = \left( \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt + \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt \right) + i \left( \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau + \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau \right). \]

We can rearrange the terms by grouping them differently:

\begin{align*} I_f(z+h)-I_f(z) = & \left( \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau \right)\\ & + \left( \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau \right). \end{align*}

The first large grouped term is precisely the definition of \(\mathrm{Err}(z,h)\) given in the lemma statement. The second large grouped term is an expression that is evaluated in lemma 212. According to that lemma,

\[ \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} f(z)\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} f(z)\, d\tau = f(z) \cdot h. \]

Substituting these two results back into our rearranged equation, we get:

\[ I_f(z+h)-I_f(z) = \mathrm{Err}(z,h) + f(z) \cdot h. \]

Swapping the terms on the right-hand side gives the final statement.

Lemma 214 Bound on error term

✓

\[ S_{horiz}(z,h) := \sup _{z.\operatorname {Re}- |h.\operatorname {Re}| \le t \le z.\operatorname {Re}+ |h.\operatorname {Re}|} |f(t + i\, z.\operatorname {Im}) - f(z)| \]

\[ S_{vert}(z,h) := \sup _{z.\operatorname {Im}- |h.\operatorname {Im}| \le \tau \le z.\operatorname {Im}+ |h.\operatorname {Im}|} |f((z+h).\operatorname {Re}+ i\tau ) - f(z)|. \]

\[ S(z,h) := \max (S_{horiz}(z,h),S_{vert}(z,h)) \]

Then the error term \(\mathrm{Err}(z,h)\) is bounded by:

\[ |\mathrm{Err}(z,h)| \le |h.\operatorname {Re}| S(z,h) + |h.\operatorname {Im}|S(z,h). \]

Proof ▶

We begin with the definition of \(\mathrm{Err}(z,h)\) from lemma 213.

\[ \mathrm{Err}(z,h) = \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt + i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau . \]

We take the modulus and apply the triangle inequality, \(|A+B| \le |A| + |B|\):

\[ |\mathrm{Err}(z,h)| \le \left| \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt \right| + \left| i \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau \right|. \]

Since \(|i|=1\), the second term simplifies to \(\left| \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau \right|\). Now we apply the ML-inequality (\(|\int _\gamma g(\zeta )d\zeta | \le \text{length}(\gamma ) \cdot \sup _{\zeta \in \gamma } |g(\zeta )|\)) to each integral.

For the first integral, the path of integration is the line segment from \(z.\operatorname {Re}\) to \((z+h).\operatorname {Re}\). The length of this path is \(|(z+h).\operatorname {Re}- z.\operatorname {Re}| = |h.\operatorname {Re}|\). The supremum of the integrand’s modulus is taken over this path. The integration variable \(t\) is in the interval between \(z.\operatorname {Re}\) and \(z.\operatorname {Re}+h.\operatorname {Re}\). This interval is contained within \([z.\operatorname {Re}- |h.\operatorname {Re}|, z.\operatorname {Re}+ |h.\operatorname {Re}|]\). Therefore, the supremum over the integration path is less than or equal to the supremum over this larger interval, which is \(S_{horiz}(z,h)\).

\[ \left| \int _{z.\operatorname {Re}}^{(z+h).\operatorname {Re}} (f(t + i\, z.\operatorname {Im}) - f(z))\, dt \right| \le |h.\operatorname {Re}| \cdot \sup _{t \text{ between } z.\operatorname {Re}, (z+h).\operatorname {Re}} |f(t + i\, z.\operatorname {Im}) - f(z)| \le |h.\operatorname {Re}| \cdot S_{horiz}(z,h). \]

For the second integral, the path is from \(z.\operatorname {Im}\) to \((z+h).\operatorname {Im}\), with length \(|(z+h).\operatorname {Im}- z.\operatorname {Im}| = |h.\operatorname {Im}|\). Similarly, the supremum of its integrand’s modulus is bounded by \(S_{vert}(z,h)\).

\[ \left| \int _{z.\operatorname {Im}}^{(z+h).\operatorname {Im}} (f((z+h).\operatorname {Re}+ i\tau ) - f(z))\, d\tau \right| \le |h.\operatorname {Im}| \cdot S_{vert}(z,h). \]

Combining these inequalities, we get:

\[ |\mathrm{Err}(z,h)| \le |h.\operatorname {Re}| S_{horiz}(z,h) + |h.\operatorname {Im}| S_{vert}(z,h). \]

By definition, \(S(z,h) = \max (S_{horiz}(z,h), S_{vert}(z,h))\). Thus, \(S_{horiz}(z,h) \le S(z,h)\) and \(S_{vert}(z,h) \le S(z,h)\). Substituting these into the inequality gives:

\[ |\mathrm{Err}(z,h)| \le |h.\operatorname {Re}| S(z,h) + |h.\operatorname {Im}| S(z,h). \]

This is the desired result.

Lemma 215 Bound on error term ratio

✓

\[ \left|\frac{\mathrm{Err}(z,h)}{h}\right| \le 2S(z,h). \]

Proof ▶

We start with the inequality from lemma 214, which holds under the given assumptions.

\[ |\mathrm{Err}(z,h)| \le |h.\operatorname {Re}| S(z,h) + |h.\operatorname {Im}|S(z,h) = (|h.\operatorname {Re}| + |h.\operatorname {Im}|) S(z,h). \]

The lemma includes the explicit assumption that \(h \neq 0\), which implies \(|h| {\gt} 0\). We can therefore divide the inequality by \(|h|\) without changing the direction of the inequality.

\[ \frac{|\mathrm{Err}(z,h)|}{|h|} \le \frac{|h.\operatorname {Re}| + |h.\operatorname {Im}|}{|h|} S(z,h). \]

Using the property that \(|\frac{A}{B}| = \frac{|A|}{|B|}\) for complex numbers, the left side is equal to \(\left|\frac{\mathrm{Err}(z,h)}{h}\right|\). For any complex number \(h = h.\operatorname {Re}+ i h.\operatorname {Im}\), we know that \(|h.\operatorname {Re}| \le \sqrt{(h.\operatorname {Re})^2 + (h.\operatorname {Im})^2} = |h|\) and \(|h.\operatorname {Im}| \le \sqrt{(h.\operatorname {Re})^2 + (h.\operatorname {Im})^2} = |h|\). Therefore, the sum is bounded: \(|h.\operatorname {Re}| + |h.\operatorname {Im}| \le |h| + |h| = 2|h|\). This gives us a bound for the fraction:

\[ \frac{|h.\operatorname {Re}| + |h.\operatorname {Im}|}{|h|} \le \frac{2|h|}{|h|} = 2. \]

Substituting this bound back into our main inequality, we get:

\[ \left|\frac{\mathrm{Err}(z,h)}{h}\right| \le 2 S(z,h). \]

This completes the proof.

Lemma 216 Limit of \(S(z,h)\) is zero

✓

\[ \lim _{h\to 0} S(z,h) = 0. \]

Proof ▶

The assumption that \(f\) is analytic on a neighborhood of \(\overline{{\mathbb D}}_{R_0}\) implies that \(f\) is continuous at every point in \(\overline{{\mathbb D}}_{R_0}\). In particular, \(f\) is continuous at \(z \in \overline{{\mathbb D}}_{R}\). By the definition of continuity at \(z\), for any \(\epsilon {\gt} 0\), there exists a \(\delta {\gt} 0\) such that for any point \(w\) satisfying \(|w-z| {\lt} \delta \), we have \(|f(w) - f(z)| {\lt} \epsilon \).

We want to show that \(\lim _{h\to 0} S(z,h) = 0\). By definition, \(S(z,h) = \max (S_{horiz}(z,h), S_{vert}(z,h))\). The limit will be zero if we can show that both \(S_{horiz}(z,h)\) and \(S_{vert}(z,h)\) tend to zero.

1. Analysis of \(S_{horiz}(z,h)\): \(S_{horiz}(z,h) = \sup _{t \in [z.\operatorname {Re}- |h.\operatorname {Re}|, z.\operatorname {Re}+ |h.\operatorname {Re}|]} |f(t + i\, z.\operatorname {Im}) - f(z)|\). Let \(w_t = t + i\, z.\operatorname {Im}\) be a point on the horizontal segment. We need to bound \(|w_t - z|\). \(|w_t - z| = |(t + i\, z.\operatorname {Im}) - (z.\operatorname {Re}+ i\, z.\operatorname {Im})| = |t - z.\operatorname {Re}|\). The supremum is over \(t\) such that \(|t - z.\operatorname {Re}| \le |h.\operatorname {Re}|\). Since \(|h.\operatorname {Re}| \le |h|\), we have \(|w_t - z| \le |h|\). If we choose \(|h| {\lt} \delta \), then for all \(t\) in the interval, \(|w_t - z| {\lt} \delta \). By the continuity of \(f\), this implies \(|f(w_t) - f(z)| {\lt} \epsilon \). Since this is true for all values in the set, their supremum must be less than or equal to \(\epsilon \). Thus, for \(|h|{\lt}\delta \), \(S_{horiz}(z,h) \le \epsilon \).

2. Analysis of \(S_{vert}(z,h)\): \(S_{vert}(z,h) = \sup _{\tau \in [z.\operatorname {Im}- |h.\operatorname {Im}|, z.\operatorname {Im}+ |h.\operatorname {Im}|]} |f((z+h).\operatorname {Re}+ i\tau ) - f(z)|\). Let \(w_\tau = (z+h).\operatorname {Re}+ i\tau = (z.\operatorname {Re}+ h.\operatorname {Re}) + i\tau \) be a point on the vertical segment. We bound \(|w_\tau - z|\). \(|w_\tau - z| = |(z.\operatorname {Re}+ h.\operatorname {Re}+ i\tau ) - (z.\operatorname {Re}+ i z.\operatorname {Im})| = |h.\operatorname {Re}+ i(\tau - z.\operatorname {Im})|\). Using the triangle inequality, \(|w_\tau - z| \le |h.\operatorname {Re}| + |i(\tau - z.\operatorname {Im})| = |h.\operatorname {Re}| + |\tau - z.\operatorname {Im}|\). The supremum is over \(\tau \) such that \(|\tau - z.\operatorname {Im}| \le |h.\operatorname {Im}|\). So, \(|w_\tau - z| \le |h.\operatorname {Re}| + |h.\operatorname {Im}|\). We know \(|h.\operatorname {Re}| + |h.\operatorname {Im}| \le 2|h|\). If we choose \(|h| {\lt} \delta /2\), then \(|w_\tau - z| \le 2|h| {\lt} \delta \). By continuity, \(|f(w_\tau ) - f(z)| {\lt} \epsilon \). Thus, for \(|h|{\lt}\delta /2\), \(S_{vert}(z,h) \le \epsilon \).

Given \(\epsilon {\gt} 0\), we can choose \(\delta ' = \delta /2\). Then for any \(h\) with \(|h| {\lt} \delta '\), both \(S_{horiz}(z,h) \le \epsilon \) and \(S_{vert}(z,h) \le \epsilon \). Therefore, \(S(z,h) = \max (S_{horiz}(z,h), S_{vert}(z,h)) \le \epsilon \) for all \(|h| {\lt} \delta '\). This satisfies the definition of the limit, so \(\lim _{h\to 0} S(z,h) = 0\).

Lemma 217 Limit of error term ratio is zero

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). Let \(z \in \overline{{\mathbb D}}_{R}\). Then

\[ \lim _{h\to 0} \frac{\mathrm{Err}(z,h)}{h} = 0. \]

Proof ▶

To prove the limit, we will use the Squeeze Theorem. The limit is taken as \(h \to 0\), so we consider \(h \neq 0\). From lemma 215, we have the inequality for the modulus of the error term ratio:

\[ \left|\frac{\mathrm{Err}(z,h)}{h}\right| \le 2S(z,h). \]

The modulus of any complex number is non-negative, so we can write:

\[ 0 \le \left|\frac{\mathrm{Err}(z,h)}{h}\right| \le 2S(z,h). \]

Now, we take the limit of all parts of the inequality as \(h \to 0\). The lower bound is constant, so \(\lim _{h\to 0} 0 = 0\). For the upper bound, we use lemma 216, which states that \(\lim _{h\to 0} S(z,h) = 0\). Therefore, \(\lim _{h\to 0} 2S(z,h) = 2 \cdot \left(\lim _{h\to 0} S(z,h)\right) = 2 \cdot 0 = 0\). Since \(\left|\frac{\mathrm{Err}(z,h)}{h}\right|\) is squeezed between two functions that both tend to 0 as \(h \to 0\), the Squeeze Theorem (Mathlib: Filter.Tendsto.squeeze’) implies that the limit of the modulus is also 0:

\[ \lim _{h\to 0} \left|\frac{\mathrm{Err}(z,h)}{h}\right| = 0. \]

A sequence of complex numbers converges to 0 if and only if the sequence of their moduli converges to 0. Therefore, we can conclude that:

\[ \lim _{h\to 0} \frac{\mathrm{Err}(z,h)}{h} = 0. \]

Lemma 218 Differentiability of \(I_f(z)\)

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(f:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\). The function \(I_f(z)\) is analyticOnNhd \(\overline{{\mathbb D}}_{R}\), and \(I'_f(z)=f(z)\) on \(\overline{{\mathbb D}}_{R}\).

Proof ▶

To show that \(I_f(z)\) is differentiable at a point \(z \in \overline{{\mathbb D}}_R\) and that its derivative is \(f(z)\), we must show that the following limit exists and equals \(f(z)\):

\[ I'_f(z) = \lim _{h\to 0} \frac{I_f(z+h)-I_f(z)}{h}. \]

We use the decomposition from lemma 213, which states:

\[ I_f(z+h)-I_f(z) = h \cdot f(z) + \mathrm{Err}(z,h). \]

For \(h \neq 0\), we can form the difference quotient by dividing by \(h\):

\[ \frac{I_f(z+h)-I_f(z)}{h} = \frac{h \cdot f(z) + \mathrm{Err}(z,h)}{h} = f(z) + \frac{\mathrm{Err}(z,h)}{h}. \]

Now, we take the limit as \(h \to 0\):

\[ I'_f(z) = \lim _{h\to 0} \left( f(z) + \frac{\mathrm{Err}(z,h)}{h} \right). \]

Using the property that the limit of a sum is the sum of the limits:

\[ I'_f(z) = \lim _{h\to 0} f(z) + \lim _{h\to 0} \frac{\mathrm{Err}(z,h)}{h}. \]

The term \(f(z)\) is constant with respect to \(h\), so its limit is \(f(z)\). From lemma 217, we know that \(\lim _{h\to 0} \frac{\mathrm{Err}(z,h)}{h} = 0\). Substituting these results back, we find:

\[ I'_f(z) = f(z) + 0 = f(z). \]

This shows that for any \(z \in \overline{{\mathbb D}}_R\), the derivative \(I'_f(z)\) exists and is equal to \(f(z)\). Since \(f\) is analytic on a neighborhood of \(\overline{{\mathbb D}}_{R_0}\), it is continuous on that neighborhood. This means \(I'_f(z) = f(z)\) is continuous on \(\overline{{\mathbb D}}_R\). A function with a continuous derivative is analytic. To show it is ‘analyticOnNhd‘ \(\overline{{\mathbb D}}_{R}\), we note that since \(R {\lt} R_0\), we can choose an \(R'\) such that \(R {\lt} R' {\lt} R_0\). The entire construction and proof holds for any \(z \in \overline{{\mathbb D}}_{R'}\). This shows that \(I_f\) is differentiable in the open disk \({\mathbb D}_{R'}\), which is an open neighborhood of \(\overline{{\mathbb D}}_{R}\). Therefore, \(I_f\) is analytic on a neighborhood of \(\overline{{\mathbb D}}_{R}\).

1.4 Complex logarithm

Lemma 219 Logarithmic derivative is analytic

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Then the function \(B'(z)/B(z)\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\).

Proof ▶

Mathlib: AnalyticOnNhd.div

Lemma 220 Antiderivative of logarithmic derivative

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Then there exists \(J: \overline{{\mathbb D}}_R\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R}\), such that \(J(0)=0\) and \(J'(z) = B'(z)/B(z)\) for all \(z \in \overline{{\mathbb D}}_R\).

Proof ▶

Take \(J=I_{B'/B}\) from lemma 218. Here \(B/B'\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) by lemma 219.

Definition 221 Auxiliary function

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Define \(J(z) := I_{B'/B}(z)\) from lemma 220. Define \(H(z) := \exp (J(z))/B(z)\).

Lemma 222 Exponential of \(I_f\) at zero

✓

Proof ▶

By lemma 220, we have \(J(0)=0\). Then \(e^0=1\) by Mathlib: Complex.exp_zero.

Lemma 223 Value of \(H\) at zero

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(H\) be the function from definition 221. Then \(H(0)=1/B(0)\).

Proof ▶

By definition 221 at \(z=0\), \(H(0) = \exp (J(0))/B(0)\). Then apply lemma 222.

Lemma 224 Logarithmic derivative identity

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). For \(J\) from lemma 220, then \(J'(z)B(z) = B'(z)\) for all \(z \in \overline{{\mathbb D}}_R\).

Proof ▶

Apply lemma 220. Since \(B(z) \ne 0\), multiply by \(B(z)\).

Lemma 225 Logarithmic derivative identity

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). For \(J\) from lemma 220, then \(J'(z)B(z) - B'(z) = 0\) for all \(z \in \overline{{\mathbb D}}_R\).

Proof ▶

By lemma 224.

Lemma 226 Derivative of \(H(z)\)

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(J\) and \(H\) be the functions from definition 221. The derivative of \(H(z)\) is given by

\[ H'(z) = \frac{(\exp (J(z)))' \cdot B(z) - B'(z) \cdot \exp (J(z))}{B(z)^2}. \]

Proof ▶

Apply Mathlib: deriv_div to \(H(z) = \exp (J(z))/B(z)\). \(B(z) \ne 0\) by assumption.

Lemma 227 Derivative of \(\exp (J(z))\)

✓

\[ (\exp (J(z)))' = J'(z) \cdot \exp (J(z)). \]

Proof ▶

Apply Mathlib: deriv.scomp_of_eq and AnalyticAt.differentiableAt to the composition \(\exp \circ I\). Here \(J\) analyticOnNhd \(\overline{{\mathbb D}}_{R}\) by lemma 220.

Lemma 228 Derivative of \(H(z)\)

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(J\) and \(H\) be the functions from definition 221. The derivative of \(H(z)\) is given by

\[ H'(z) = \frac{\big(J'(z) B(z) - B'(z)\big)\exp (J(z))}{B(z)^2}. \]

Proof ▶

By ??.

Lemma 229 Derivative of \(H(z)\) is 0

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(J\) and \(H\) be the functions from definition 221. Then \(H'(z) = 0\) for all \(z \in \overline{{\mathbb D}}_R\).

Proof ▶

Apply ??.

Lemma 230 \(H(z)\) is constant

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(H\) be from definition 221. Then \(H(z)=H(0)\) for all \(z\in \overline{{\mathbb D}}_R\).

Proof ▶

Apply Mathlib: is_const_of_fderiv_eq_zero to lemma 229 with \(H(z)\) on the connected set \(\overline{{\mathbb D}}_R\).

Lemma 231 \(H=1\)

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\), \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(H\) be the function from definition 221. Then \(H(z)=1/B(0)\) for all \(z \in \overline{{\mathbb D}}_R\).

Proof ▶

Apply ??.

Lemma 232 Existence of analytic logarithm

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) with \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). For \(J\) from lemma 220, then \(B(z) = B(0)\exp (J(z))\) for all \(z \in \overline{{\mathbb D}}_R\).

Proof ▶

By ??.

Lemma 233 Modulus of \(\exp (J(z))\)

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), and assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) and \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Let \(J\) be the function from lemma 220. Then for any \(z \in \overline{{\mathbb D}}_R\),

\[ |\exp (J(z))| = \exp (\Re (J(z))). \]

Proof ▶

Apply Mathlib: Complex.abs_exp with \(w = J(z)\).

Lemma 234 Modulus of \(B(z)\) in product form

✓

Proof ▶

By lemma 232, then apply modulus and Mathlib: abs_mul.

Lemma 235 Modulus of \(\exp (J(z))\)

✓

Proof ▶

By ??.

Lemma 236 Logarithm of modulus as sum

✓

Proof ▶

Apply lemma 235 then Mathlib: Real.log_mul.

Lemma 237 Real logarithm of modulus difference

✓

Proof ▶

Apply lemma 236 and Mathlib: Real.log_exp to \(x=\Re (J(z))\).

Lemma 238 Logarithm of an analytic function

✓

Let \(0{\lt}R{\lt}R_0{\lt}1\), assume \(B:\overline{{\mathbb D}}_{R_0}\to \mathbb {C}\) is analyticOnNhd \(\overline{{\mathbb D}}_{R_0}\) with \(B(z) \ne 0\) for all \(z \in \overline{{\mathbb D}}_{R_0}\). Then there exists \(J_B: \overline{{\mathbb D}}_R\to \mathbb {C}\) analyticOnNhd \(\overline{{\mathbb D}}_{R}\), such that \(J_B(0)=0\), and \(J_B'(z) = B'(z)/B(z)\) and \(\log |B(z)| - \log |B(0)| = \Re (J_B(z))\) for all \(z \in \overline{{\mathbb D}}_R\).

Proof ▶

Apply ??.