How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 15 results · all verified · 11 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Analyticity of Holomorphic Functions; Liouville and Morera

1 · Prerequisites

2 · Summary

Cauchy's circle formula and its higher-derivative form recover a holomorphic function from values on a compactly contained circle. Complex power-series sums are already known to be holomorphic, with unique derivative coefficients, while Goursat's theorem supplies zero integrals around contained triangles. Compact convergence provides the precise meaning of local uniform convergence used for sequences and series of holomorphic functions.

Expanding the Cauchy kernel proves that holomorphic and analytic functions are the same and identifies zero order with local factorization. Cauchy's estimates then yield Liouville's theorem, polynomial rigidity under algebraic growth, and the analytic proof of the fundamental theorem of algebra. Morera gives the converse triangle criterion; concentric-disc estimates give Weierstrass convergence with derivative convergence. Finite parameter integrals remain holomorphic, holomorphic functions satisfy the circular mean-value property, and every nonconstant entire function has dense image.

3 · Logical flowchart

4 · Definitions, theorems and proofs

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Locally uniform convergence on an open subset of the complex plane is compact convergence

Remark

Let $Ω \subseteq C$ be open, and let $f_{n}, f : Ω \to C$ be continuous. The sequence $(f_{n})$ converges locally uniformly to $f$ when each $a \in Ω$ has an open neighbourhood $V \subseteq Ω$ on which $f_{n} \to f$ uniformly. This is equivalent to uniform convergence on every compact subset of $Ω$ , hence to convergence in the topology of compact convergence of The topology of compact convergence on $C (X, Y)$ for metric $X$ and $Y$ : uniform convergence on each compact subset of $X$ .

Indeed, suppose first that convergence is uniform on compact subsets. Openness gives $r > 0$ with the closed disc $\overline{D} (a, r) \subseteq Ω$ after shrinking an available ball; this closed disc is compact by Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, so convergence is uniform on the neighbourhood $D (a, r)$ . Conversely, suppose convergence is uniform on a neighbourhood $V_{x}$ of every $x \in Ω$ . For a compact $K \subseteq Ω$ and $ε > 0$ , the sets $V_{x}$ cover $K$ , and compactness in the ambient space (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it) gives a finite subcover. Taking the largest of the corresponding finitely many convergence thresholds makes $∣ f_{n} - f ∣ < ε$ throughout $K$ . The empty compact set satisfies the uniform condition vacuously.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Real-analytic maps between open subsets of the coordinate plane

Definition

A smooth map $F = (u, v) : U \to R^{2}$ on an open set $U \subseteq R^{2}$ is real analytic when, at every $a \in U$ , both components equal their total-degree Taylor series on some neighbourhood of $a$ .

More explicitly, write multi-indices, their factorials, and the derivatives $D^{α}$ as in $C^{k}$ maps and multi-index derivative notation in Euclidean space and The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ . For each $a \in U$ there must be a neighbourhood on which, for $h = (h_{0}, h_{1})$ with $a + h \in U$ ,

$u (a + h) = \sum_{n \geq 0} \sum_{∣ α ∣ = n} \frac{D^{α} u (a)}{α!} h^{α}, v (a + h) = \sum_{n \geq 0} \sum_{∣ α ∣ = n} \frac{D^{α} v (a)}{α!} h^{α} .$

Each inner sum is finite (Finite sums and finite products, by recursion), and each outer sum is a real series in the sense of Series, partial sums, convergence and the sum, divergence, and the tail series. The coordinate functions $u$ and $v$ are the components of the map into $R^{2}$ under the convention of Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions. Equality with the displayed series includes convergence to the stated component value; convergence is not presumed merely from smoothness.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The Taylor series of a holomorphic function at a point

Definition

Let $f$ be holomorphic on an open set $Ω \subseteq C$ , and let $a \in Ω$ . The Taylor series of $f$ at $a$ is $\sum_{n \geq 0} f^{(n)} (a) (z - a)^{n} / n!$ .

Every derivative $f^{(n)} (a)$ exists by All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle, and $n!$ is the positive factorial of The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , so each coefficient

$c_{n} : = \frac{f^{(n)} (a)}{n!}$

is a well-defined complex number. The resulting complex power series is understood according to Complex series, absolute convergence, complex power series, and radius of convergence. This definition names the formal series; its convergence and equality with $f$ are conclusions of the Taylor expansion theorem.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The order of a zero of a holomorphic function

Definition

Let $f$ be holomorphic on a neighbourhood of $a$ , and let $(c_{n})$ be the coefficients of its Taylor series at $a$ (The Taylor series of a holomorphic function at a point). The order ${ord}_{a} (f)$ is the least natural $n$ for which the $n$ th Taylor coefficient is nonzero, and is $+ \infty$ when every Taylor coefficient is zero.

If the set ${n \in N : c_{n} \neq 0}$ is nonempty, its least element exists and is unique by The well-ordering principle. If the set is empty, the separate value $+ \infty \in \overline{R}$ is supplied by The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined. Thus the cases are exhaustive and do not overlap. When $f (a) \neq 0$ , the order is $0$ ; when $f (a) = 0$ and the order is finite, it is a positive natural number; the infinite value records that every Taylor coefficient vanishes rather than naming a natural exponent.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

A holomorphic function equals its Taylor series throughout the largest centred disc in its domain

Statement

Let $Ω \subseteq C$ be open, let $f : Ω \to C$ be holomorphic, and let $a \in Ω$ . Put

$ρ_{a} : = {\begin{cases} d (a, C ∖ Ω), & C ∖ Ω \neq \emptyset, \\ + \infty, & Ω = C . \end{cases}$

Then $ρ_{a} > 0$ , the disc $D (a, ρ_{a})$ is the largest centred open disc contained in $Ω$ , with $D (a, + \infty) = C$ , and

$f (z) = \sum_{n \geq 0} \frac{f^{(n)} (a)}{n!} (z - a)^{n} (∣ z - a ∣ < ρ_{a}) .$

Every holomorphic function equals its Taylor series throughout the largest centred open disc contained in its domain.

Facts & Assumptions

Given: An open set $Ω \subseteq C$ , a holomorphic function $f : Ω \to C$ , and a point $a \in Ω$ ; the Taylor series convention of The Taylor series of a holomorphic function at a point and the whole-plane element $+ \infty$ of The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined.

[L1]

For a point $x$ and a nonempty subset $A$ of a metric space, the distance $d (x, A)$ is the greatest lower bound of ${d (x, y) : y \in A}$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L2]

If $f$ is holomorphic on $D (a, R)$ , $0 < r < R$ , $∣ z - a ∣ < r$ , and $γ (t) = a + r \exp (i t)$ , then $f (z) = (2 π i)^{- 1} \int_{γ} f (ζ) / (ζ - z) d ζ$ (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[L3]

Complex modulus is multiplicative, vanishes exactly at zero, and satisfies $∣ u + v ∣ \leq ∣ u ∣ + ∣ v ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L4]

If a real $q$ satisfies $∣ q ∣ < 1$ , then $q^{k} \to 0$ (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L5]

Uniform convergence of continuous integrands on the trace of a fixed rectifiable contour permits passage of the limit through the complex line integral (A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral).

[L6]

For every natural $n$ , Cauchy's higher-derivative formula gives $f^{(n)} (a) = n! (2 π i)^{- 1} \int_{γ} f (ζ) / (ζ - a)^{n + 1} d ζ$ on a compactly contained circle (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).

[L7]

A holomorphic function is continuous (Complex differentiability at a point implies continuity there).

[L8]

Closed bounded subsets of the Euclidean plane, and in particular circles of positive radius, are compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L9]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

technique · direct

1.1givenL1

If $Ω \neq C$ , openness gives $s > 0$ with $D (a, s) \subseteq Ω$ , so every $w \in C ∖ Ω$ has $∣ w - a ∣ \geq s$ and [L1] gives $ρ_{a} \geq s > 0$ ; moreover $∣ z - a ∣ < ρ_{a}$ forces $z \in Ω$ , while every $R > ρ_{a}$ contains a point of the complement by the defining greatest-lower-bound property. If $Ω = C$ , the stated $+ \infty$ convention gives the same largest-disc conclusion.

2.1step 1.1L2choose

Fix $z$ with $∣ z - a ∣ < ρ_{a}$ , and choose $r = (∣ z - a ∣ + ρ_{a}) / 2$ when $ρ_{a}$ is finite and $r = ∣ z - a ∣ + 1$ otherwise; then $∣ z - a ∣ < r < ρ_{a}$ , the radius- $r$ circle and its interior lie in $Ω$ by step 1.1, and [L2] gives $f (z) = (2 π i)^{- 1} \int_{γ} f (ζ) / (ζ - z) d ζ$ .

3.1step 2.1L3L4L7L8L9algebra

On $∣ ζ - a ∣ = r$ , the finite geometric identity gives $1 / (ζ - z) = \sum_{n = 0}^{N} (z - a)^{n} / (ζ - a)^{n + 1} + E_{N} (ζ)$ with $∣ E_{N} (ζ) ∣ \leq q^{N + 1} / (r - ∣ z - a ∣)$ for $q = ∣ z - a ∣ / r < 1$ ; [L7], [L8], and [L9] bound $∣ f ∣$ on the circle, so [L3] and [L4] make $f E_{N} \to 0$ uniformly there, including the case $z = a$ where $q = 0$ .

4.1step 2.1step 3.1L5algebra

By [L5], step 3.1 may be integrated term by term in the limit, and step 2.1 becomes $f (z) = \sum_{n \geq 0} (z - a)^{n} (2 π i)^{- 1} \int_{γ} f (ζ) / (ζ - a)^{n + 1} d ζ$ .

5.1step 1.1step 2.1step 4.1L6choose

Choose a radius $R$ with $r < R < ρ_{a}$ when $ρ_{a}$ is finite, and take $R = r + 1$ in the whole-plane case. Then $f$ is holomorphic on $D (a, R)$ and the radius- $r$ circle is compactly contained there, so for every natural $n$ , [L6] identifies the integral coefficient in step 4.1 with $f^{(n)} (a) / n!$ , including $n = 0$ and $0! = 1$ .

6.1step 1.1step 5.1∎

Since the point $z$ was arbitrary in the disc identified in step 1.1, step 5.1 proves the displayed Taylor equality throughout the largest centred open disc contained in $Ω$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

A complex function is holomorphic if and only if it is analytic

Statement

Let $U \subseteq C$ be open and let $f : U \to C$ . Then $f$ is holomorphic on $U$ if and only if it is analytic on $U$ in the local power-series sense of Complex analytic functions as locally representable by convergent power series.

Facts & Assumptions

Given: An open set $U \subseteq C$ and a function $f : U \to C$ .

[L1]

Every holomorphic function equals its Taylor series throughout the largest centred open disc contained in its domain (A holomorphic function equals its Taylor series throughout the largest centred disc in its domain).

[L2]

A function is analytic on an open set exactly when every point has a contained open disc on which the function equals a convergent complex power series centred at that point (Complex analytic functions as locally representable by convergent power series).

[L3]

Every function analytic on an open subset of $C$ is holomorphic there (Every complex analytic function is holomorphic).

Proof

technique · direct

1.1L1L2

For the holomorphic-to-analytic direction, if $f$ is holomorphic and $a \in U$ , [L1] gives a positive-radius disc about $a$ on which $f$ equals its Taylor series, so [L2] makes $f$ analytic at $a$ and hence on $U$ .

1.2L2L3

For the analytic-to-holomorphic direction, the local power-series hypothesis of [L2] is exactly the hypothesis of [L3], which makes $f$ holomorphic on the same open set $U$ .

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove both implications; when $U = \emptyset$ , both pointwise predicates hold vacuously, so the equivalence also includes the empty open set.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Holomorphic functions are real analytic and smooth in their two real coordinates

Statement

Let $U \subseteq C$ be open and let $f = u + i v : U \to C$ be holomorphic. Under the coordinate identification $C = R^{2}$ , the map $(u, v) : U \to R^{2}$ is real analytic in the sense of Real-analytic maps between open subsets of the coordinate plane and is of class $C^{k}$ for every natural $k$ , hence smooth.

Facts & Assumptions

Given: The identification of the complex plane with the real coordinate plane from $C$ is the real coordinate plane, with coordinate arithmetic, an open set $U$ , and a holomorphic function $f = u + i v$ on $U$ .

[L1]

[L2]

For complex $z, w$ and a natural $n$ , $(z + w)^{n} = \sum_{p \leq n} (\binom{n}{p}) z^{p} w^{n - p}$ , with each binomial coefficient regarded as a complex scalar (The binomial theorem over the complex field).

[L3]

A smooth planar map is real analytic when each component equals its total-degree Taylor series on a neighbourhood of every point (Real-analytic maps between open subsets of the coordinate plane).

[L4]

A holomorphic function has complex derivatives of every natural order locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).

[L5]

If $f = u + i v$ is complex differentiable, then $f^{'} = u_{x} + i v_{x} = v_{y} - i u_{y}$ and the Cauchy–Riemann equations hold (Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\overset{ˉ}{z}} f = 0$ , or with the Cauchy–Riemann equations).

[L6]

A real function is $C^{k}$ when every coordinate-derivative word of length at most $k$ , including the word of length zero, exists and is continuous ( $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[L7]

Every complex power series converges absolutely and uniformly on closed subdiscs strictly inside its disc of convergence (A complex power series converges absolutely and uniformly on every closed subdisc strictly inside its disc of convergence).

[L8]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L9]

If $p \leq n$ , then the complex scalar corresponding to $(\binom{n}{p})$ is $n! / (p! (n - p)!)$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ ).

Proof

technique · direct

1.1L1

Fix $a \in U$ . By [L1], there is $R > 0$ such that $f (a + h) = \sum_{n \geq 0} c_{n} h^{n}$ for $∣ h ∣ < R$ , where $c_{n} = f^{(n)} (a) / n!$ .

2.1step 1.1L2L7algebra

Write $h = x + i y$ . By [L2], $h^{n} = \sum_{p \leq n} (\binom{n}{p}) x^{p} (i y)^{n - p}$ ; if $∣ x ∣ + ∣ y ∣ < R$ , [L7] and the binomial identity give absolute convergence of the resulting total-degree series because the sum of the absolute values in degree $n$ is $∣ c_{n} ∣ (∣ x ∣ + ∣ y ∣)^{n}$ .

3.1step 1.1step 2.1L4L5L9algebra

From [L5], $\partial_{x} f = f^{'}$ and $\partial_{y} f = i f^{'}$ ; induction using [L4] therefore gives $\partial_{x}^{p} \partial_{y}^{q} f (a) = i^{q} f^{(p + q)} (a)$ . Taking $n = p + q$ in step 2.1 and using [L9], the coefficient of $x^{p} y^{q}$ is $c_{p + q} (\binom{p + q}{p}) i^{q} = D^{(p, q)} f (a) / (p! q!)$ .

4.1step 2.1step 3.1

Taking real and imaginary parts in the absolutely convergent expansion of step 2.1, and using the coefficient identification of step 3.1, gives the total-degree Taylor series of $u$ and $v$ on $∣ x ∣ + ∣ y ∣ < R$ .

5.1step 3.1step 4.1L3L4L5L6L8∎

More generally, every coordinate-derivative word with $p$ occurrences of $x$ and $q$ occurrences of $y$ is the corresponding real or imaginary component of $i^{q} f^{(p + q)}$ ; [L4] makes the next complex derivative exist, [L8] makes every $f^{(p + q)}$ continuous, and the word of length zero is $f$ itself, so [L6] makes both components $C^{k}$ for every natural $k$ . Thus the map is smooth, and step 4.1 now satisfies the opening hypothesis of [L3], proving real analyticity as well.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Agreement of the power-series and Cauchy-integral formulas for Taylor coefficients

Remark

For the Taylor series of The Taylor series of a holomorphic function at a point, the coefficient of $(z - a)^{n}$ is $f^{(n)} (a) / n!$ . This agrees with the coefficient formula for an arbitrary convergent complex power-series representation in The coefficients of a complex power series are its derivatives at the centre divided by the corresponding factorials. If $0 < r$ is small enough that the circle $∣ ζ - a ∣ = r$ and its interior lie in the holomorphy domain, All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle gives the same coefficient as

$\frac{f^{(n)} (a)}{n!} = \frac{1}{2 π i} \int_{∣ ζ - a ∣ = r} \frac{f (ζ)}{(ζ - a)^{n + 1}} d ζ .$

Thus the derivative and contour formulas name the coefficients of the expansion established by A holomorphic function equals its Taylor series throughout the largest centred disc in its domain; neither is an additional choice of series.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

The order of a zero is the exponent in its local holomorphic factorization

Statement

Let $f$ be holomorphic on a neighbourhood of $a$ . A holomorphic function has finite order $m$ at $a$ if and only if, on some neighbourhood of $a$ , it has the form $f (z) = (z - a)^{m} g (z)$ with $g$ holomorphic and $g (a) \neq 0$ .

Moreover, ${ord}_{a} (f) = + \infty$ if and only if $f$ vanishes on a neighbourhood of $a$ .

Facts & Assumptions

Given: A function $f$ holomorphic on a neighbourhood of $a$ .

[L1]

The order ${ord}_{a} (f)$ is the least natural $n$ for which the $n$ th Taylor coefficient is nonzero, and is $+ \infty$ when every Taylor coefficient is zero (The order of a zero of a holomorphic function).

[L2]

[L3]

Every function analytic on an open subset of $C$ is holomorphic there (Every complex analytic function is holomorphic).

[L4]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L5]

A convergent complex power-series representation has uniquely determined coefficients, equal to the derivatives at its centre divided by the corresponding factorials (The coefficients of a complex power series are its derivatives at the centre divided by the corresponding factorials).

Proof

technique · direct

1.1L1L2

For the finite-order-to-factorization direction, suppose ${ord}_{a} (f) = m < + \infty$ and write the Taylor expansion from [L2] as $f (z) = \sum_{n \geq 0} c_{n} (z - a)^{n}$ ; [L1] gives $c_{0} = \dots = c_{m - 1} = 0$ and $c_{m} \neq 0$ , so formally $f (z) = (z - a)^{m} \sum_{k \geq 0} c_{m + k} (z - a)^{k}$ .

1.2L1L2L5algebra

For the factorization-to-finite-order direction, suppose $f (z) = (z - a)^{m} g (z)$ locally with $g$ holomorphic and $g (a) \neq 0$ ; expanding $g (z) = \sum_{k \geq 0} b_{k} (z - a)^{k}$ by [L2] gives $b_{0} = g (a) \neq 0$ . Multiplication by $(z - a)^{m}$ gives a convergent power-series representation of $f$ whose coefficients below degree $m$ vanish and whose degree- $m$ coefficient is $b_{0}$ ; [L5] identifies these with the Taylor coefficients of $f$ , so [L1] gives ${ord}_{a} (f) = m$ .

2.1step 1.1L3algebra

For the finite-order-to-factorization direction, define $g (z) = \sum_{k \geq 0} c_{m + k} (z - a)^{k}$ on the Taylor disc: at $z = a$ the series has value $c_{m}$ , and away from $a$ its absolute convergence follows by dividing the absolutely convergent tail of the series in step 1.1 by $∣ z - a ∣^{m}$ ; thus $g$ is analytic and [L3] makes it holomorphic.

3.1step 2.1L4

For the finite-order-to-factorization direction, step 2.1 gives $g (a) = c_{m} \neq 0$ , and [L4] supplies a smaller neighbourhood on which $g$ remains nonzero; hence the required local factorization holds, including $m = 0$ where the factor is $1$ .

4.1L1L2∎

For the infinite-order equivalence, [L1] says infinite order means that every Taylor coefficient is zero, and [L2] then makes $f$ vanish on a neighbourhood of $a$ ; conversely, if $f$ vanishes on a neighbourhood, all of its derivatives and hence all of its Taylor coefficients at $a$ are zero, so [L1] gives infinite order.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Cauchy's inequalities bound the Taylor coefficients by the circle supremum

Statement

Let $f$ be holomorphic on $D (a, R)$ , let $0 < r < R$ , and suppose $M \geq 0$ satisfies $∣ f (ζ) ∣ \leq M$ whenever $∣ ζ - a ∣ = r$ . If $c_{n} = f^{(n)} (a) / n!$ is the $n$ th coefficient of the Taylor series of $f$ at $a$ , then

$∣ c_{n} ∣ \leq \frac{M}{r^{n}} (n \in N) .$

If $∣ f (ζ) ∣ \leq M$ on $∣ ζ - a ∣ = r$ , then the $n$ th Taylor coefficient $c_{n}$ satisfies $∣ c_{n} ∣ \leq M / r^{n}$ .

Facts & Assumptions

Given: A holomorphic function $f$ on $D (a, R)$ , a radius $0 < r < R$ , a bound $M \geq 0$ on the radius- $r$ circle, and a natural $n$ .

[L1]

The Taylor series of $f$ at $a$ is $\sum_{n \geq 0} f^{(n)} (a) (z - a)^{n} / n!$ (The Taylor series of a holomorphic function at a point).

[L2]

Under the hypotheses above, $∣ f^{(n)} (a) ∣ \leq n! M / r^{n}$ for every natural $n$ (Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle).

Proof

technique · direct

1.1L1L2

By [L1], $c_{n} = f^{(n)} (a) / n!$ , while [L2] gives $∣ f^{(n)} (a) ∣ \leq n! M / r^{n}$ .

2.1step 1.1algebra∎

Since $n!$ is positive and $r > 0$ , division in step 1.1 is legitimate and yields $∣ c_{n} ∣ \leq M / r^{n}$ ; for $n = 0$ this is $∣ f (a) ∣ \leq M$ , and the same calculation permits $M = 0$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Liouville's theorem: every bounded entire function is constant

Statement

Every bounded entire function is constant.

More explicitly, if $f : C \to C$ is holomorphic and there is a real $M \geq 0$ such that $∣ f (z) ∣ \leq M$ for every $z \in C$ , then $f$ is constant.

Facts & Assumptions

Given: An entire function $f : C \to C$ and a real $M \geq 0$ with $∣ f (z) ∣ \leq M$ for every $z$ ; the Euclidean identification of $C = R [x] / (x^{2} + 1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves and the definition of complex domain in A complex domain is a nonempty connected open subset of $C$ .

[L1]

If $f$ is holomorphic on $D (a, R)$ , $0 < r < R$ , and $∣ f ∣ \leq M$ on the radius- $r$ circle, then $∣ f^{(n)} (a) ∣ \leq n! M / r^{n}$ for every natural $n$ (Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle).

[L2]

A holomorphic function on a complex domain whose derivative vanishes everywhere is constant (A holomorphic function with zero derivative on a domain is constant).

[L3]

The Euclidean plane $R^{2}$ is polygonally connected and connected ( $R^{n}$ is polygonally connected, connected, locally path-connected and locally connected).

Proof

technique · direct

1.1givenL1

Fix $a \in C$ and $r > 0$ . Since $f$ is holomorphic on $D (a, r + 1)$ and its modulus is at most $M$ on the radius- $r$ circle, [L1] with derivative order one gives $∣ f^{'} (a) ∣ \leq M / r$ .

1.2givenL3

Under the identification in the given data, [L3] makes $C$ connected; it is also nonempty and open in itself, so it is a complex domain.

2.1step 1.1choosealgebra

If $∣ f^{'} (a) ∣ > 0$ , choose $r = M / ∣ f^{'} (a) ∣ + 1$ ; then $M / r < ∣ f^{'} (a) ∣$ , contradicting step 1.1, so $f^{'} (a) = 0$ .

3.1step 2.1step 1.2L2∎

Since $a$ was arbitrary, step 2.1 gives $f^{'} = 0$ throughout the domain of step 1.2, and [L2] makes $f$ constant; this also covers $M = 0$ and every constant entire function.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

An entire function of polynomial growth is a polynomial

Statement

Let $f : C \to C$ be entire. Suppose there are real numbers $C, N \geq 0$ such that

$∣ f (z) ∣ \leq C (1 + ∣ z ∣)^{N} (z \in C),$

where real powers have the convention of Real powers for positive bases, with the zero-base positive-exponent convention. Put $m = ⌊ N ⌋$ . Then there are complex coefficients $c_{0}, \dots, c_{m}$ such that

$f (z) = \sum_{k = 0}^{m} c_{k} z^{k} (z \in C) .$

Thus $f$ is a polynomial, and if it is nonzero its degree is at most $⌊ N ⌋$ .

Facts & Assumptions

Given: An entire function $f$ and real constants $C, N \geq 0$ satisfying the displayed growth bound.

[L1]

If $f$ is holomorphic on $D (a, R_{0})$ , $0 < r < R_{0}$ , and $∣ f (ζ) ∣ \leq M$ on $∣ ζ - a ∣ = r$ , then the $n$ th Taylor coefficient $c_{n}$ satisfies $∣ c_{n} ∣ \leq M / r^{n}$ (Cauchy's inequalities bound the Taylor coefficients by the circle supremum).

[L2]

For $a > 0$ and real $x$ , the real power is $a^{x} = \exp (x \log a)$ ; zero-base powers are defined only for positive exponents (Real powers for positive bases, with the zero-base positive-exponent convention).

[L3]

Positive-base real powers satisfy $a^{r + s} = a^{r} a^{s}$ and $(a b)^{r} = a^{r} b^{r}$ (The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

[L4]

The natural logarithm is the inverse of the exponential on the positive reals (The natural logarithm as the inverse of the exponential function).

[L5]

The exponential tends to $0$ at $- \infty$ and to $+ \infty$ at $+ \infty$ (The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ ).

[L6]

Every entire function equals its Taylor series at the origin on the whole complex plane (A holomorphic function equals its Taylor series throughout the largest centred disc in its domain).

[L7]

For every real $x$ there is a unique integer $⌊ x ⌋$ satisfying $⌊ x ⌋ \leq x < ⌊ x ⌋ + 1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

[L8]

The exponential function is strictly increasing on $R$ (The exponential function is strictly increasing).

Proof

technique · direct

1.1givenL1

Let $f (z) = \sum_{n \geq 0} c_{n} z^{n}$ be its Taylor series at $0$ , fix a natural $n > N$ , and take any real $R \geq 1$ ; the growth hypothesis bounds $∣ f ∣$ on $∣ ζ ∣ = R$ by $C (1 + R)^{N}$ , so [L1], applied with outer radius $R + 1$ , gives $∣ c_{n} ∣ \leq C (1 + R)^{N} / R^{n}$ .

2.1step 1.1L2L3L4L5L8algebra

Since $R \geq 1$ gives $1 + R \leq 2 R$ , [L2], [L3], [L4], and [L8] give $∣ c_{n} ∣ \leq C 2^{N} R^{N - n} = C 2^{N} \exp (- (n - N) \log R)$ ; by [L4], [L5], and [L8], $\log R \to + \infty$ as $R \to + \infty$ , so the right side tends to $0$ , forcing $c_{n} = 0$ .

3.1step 2.1L6

Step 2.1 applies to every natural $n > N$ , and [L6] represents $f$ globally by its Taylor series, so all terms with index exceeding $N$ vanish and the series truncates.

4.1step 3.1L7

Put $m = ⌊ N ⌋$ . By [L7], $m \leq N < m + 1$ , so every natural $n \geq m + 1$ satisfies $n > N$ and has $c_{n} = 0$ by step 3.1; because $N \geq 0$ , the integer $m$ is a natural number, and the displayed finite polynomial has no term above $m$ .

5.1step 3.1step 4.1algebra∎

If $C = 0$ , the hypothesis gives $f = 0$ directly; if $N = 0$ , step 4.1 gives $m = 0$ and $f$ is constant. In every case step 4.1 proves the stated polynomial representation, with the degree qualification interpreted only for a nonzero polynomial.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Fundamental theorem of algebra by Liouville's theorem

Statement

Every nonconstant complex polynomial has a complex root.

This proof uses Liouville's theorem and is independent of the minimum-modulus proof cited in the accompanying agreement remark.

Facts & Assumptions

Given: A nonconstant complex polynomial $p$ .

[L1]

If $P, Q$ are complex polynomials, then $P / Q$ is holomorphic on the open set where $Q$ does not vanish (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[L2]

If $p$ is a nonconstant complex polynomial, then $∣ p (z) ∣ \to \infty$ as $∣ z ∣ \to \infty$ (A nonconstant complex polynomial tends to infinite modulus and attains a global minimum modulus).

[L3]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L4]

Complex modulus is multiplicative, nonnegative, and zero exactly at zero, and it satisfies the triangle inequality (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L5]

Under $C = R^{2}$ , the metric $d_{C} (z, w) = ∣ z - w ∣$ is the Euclidean metric (The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane).

[L6]

A subset of Euclidean space is compact if and only if it is closed and bounded (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L7]

[L8]

Every bounded entire function is constant (Liouville's theorem: every bounded entire function is constant).

Proof

technique · contradiction

1.1givenassume-contra

Suppose, for contradiction, that $p$ has no complex root.

2.1step 1.1L1

The denominator $p$ is then nonzero throughout $C$ , so [L1] makes $g : = 1 / p$ entire.

3.1step 2.1L2L4choosealgebra

By [L2], choose $R \geq 1$ such that $∣ p (z) ∣ \geq 1$ whenever $∣ z ∣ \geq R$ ; then step 2.1 and [L4] give $∣ g (z) ∣ = 1 / ∣ p (z) ∣ \leq 1$ on that exterior region.

3.2step 2.1L3L4algebra

By step 2.1 and [L3], $g$ is continuous; the inequality $∣ ∣ u ∣ - ∣ v ∣ ∣ \leq ∣ u - v ∣$ derived from [L4] makes the real-valued function $∣ g ∣$ continuous.

4.1step 3.1L4L5L6algebra

The closed disc $K = {z : ∣ z ∣ \leq R}$ contains $0$ , is bounded, and is closed because $∣ ∣ z ∣ - ∣ w ∣ ∣ \leq ∣ z - w ∣$ ; by [L5] it is a nonempty closed bounded subset of $R^{2}$ , so [L6] makes it compact.

5.1step 3.2step 4.1L7

Applying [L7] to the continuous function $∣ g ∣$ from step 3.2 on the compact set from step 4.1 gives a finite maximum $M \geq 0$ with $∣ g (z) ∣ \leq M$ for $z \in K$ .

6.1step 3.1step 5.1algebra

If $∣ z ∣ \leq R$ , step 5.1 gives $∣ g (z) ∣ \leq M$ , while if $∣ z ∣ \geq R$ , step 3.1 gives $∣ g (z) ∣ \leq 1$ ; hence $∣ g (z) ∣ \leq \max {M, 1}$ on the whole plane, with the boundary $∣ z ∣ = R$ covered by both estimates.

7.1step 2.1step 6.1L8

The function $g$ is entire by step 2.1 and bounded by step 6.1, so [L8] makes it constant.

8.1step 1.1step 2.1step 7.1L4algebradischarge-contradiction∎

The constant value of $g = 1 / p$ is nonzero by [L4], so $p = 1 / g$ is constant, contradicting the given nonconstancy; the assumption of step 1.1 is false, and $p$ has a complex root.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Agreement of the Liouville and minimum-modulus proofs of the fundamental theorem of algebra

Remark

The theorem Fundamental theorem of algebra by Liouville's theorem applies Liouville's theorem to the reciprocal of a hypothetical zero-free polynomial. The theorem Fundamental theorem of algebra: every nonconstant complex polynomial has a complex root establishes the same root-existence statement by descending from a positive minimum of the polynomial's modulus. The routes are independent: the Liouville argument does not cite the minimum-modulus theorem, and the minimum-modulus argument does not use Liouville's theorem.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The edgewise Riemann integral around a complex triangle for an integrable pullback

Definition

For an ordered complex triangle and a function on its boundary trace, if the pullback along each affine edge multiplied by that edge's constant velocity is Riemann integrable, define the edgewise triangle integral to be the sum of those three complex Riemann integrals.

Precisely, let the directed edges $ℓ_{a b}$ , $ℓ_{b c}$ , and $ℓ_{c a}$ be those of Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter, and let $f$ be defined on their combined trace. When the functions

$t ⟼ f (ℓ_{a b} (t)) (b - a), t ⟼ f (ℓ_{b c} (t)) (c - b), t ⟼ f (ℓ_{c a} (t)) (a - c)$

are Riemann integrable on $[0, 1]$ as maps into $C = R^{2}$ ( $C$ is the real coordinate plane, with coordinate arithmetic, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral), put

$\int_{\partial Δ [a, b, c]}^{e d g e} f (z) d z : = \int_{0}^{1} f (ℓ_{a b} (t)) (b - a) d t + \int_{0}^{1} f (ℓ_{b c} (t)) (c - b) d t + \int_{0}^{1} f (ℓ_{c a} (t)) (a - c) d t .$

The integrability hypothesis makes every term a uniquely defined complex number, so the displayed sum is well-defined. If $f$ is continuous on the trace, For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals identifies this edgewise value with the published contour integral $\int_{\partial Δ [a, b, c]} f (z) d z$ . Constant edges cause no ambiguity because their velocity is zero.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Morera's theorem: vanishing triangle integrals characterize holomorphy among continuous functions

Statement

A continuous function on an open subset of $C$ is holomorphic if and only if its integral around the boundary of every filled triangle contained in the open set is zero.

Precisely, if $Ω \subseteq C$ is open and $f : Ω \to C$ is continuous, then

$f is holomorphic on Ω ⟺ \int_{\partial Δ [a, b, c]} f (z) d z = 0 whenever Δ [a, b, c] \subseteq Ω .$

Repeated or collinear vertices are permitted.

Facts & Assumptions

Given: An open set $Ω \subseteq C$ and a continuous function $f : Ω \to C$ .

[L1]

A filled triangle $Δ [a, b, c]$ has positively oriented boundary $ℓ_{a b} * ℓ_{b c} * ℓ_{c a}$ , and repeated or collinear vertices are allowed (Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter).

[L2]

On an open set star-shaped with respect to a point, a continuous function whose integral vanishes around every contained filled triangle has a holomorphic primitive $F$ satisfying $F^{'} = f$ (Vanishing integrals around triangles construct a primitive for a continuous function on a star-shaped domain).

[L3]

Every holomorphic function has complex derivatives of every natural order locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).

[L4]

A holomorphic function has zero integral around every filled triangle contained in its open domain, including degenerate triangles (Goursat's triangle theorem: a holomorphic function integrates to zero around every triangle contained in its domain).

Proof

technique · direct

1.1givenL1

For the vanishing-integrals-to-holomorphy direction, fix $a \in Ω$ and choose $r > 0$ with $\overline{D} (a, r) \subseteq Ω$ ; the disc $D (a, r)$ is star-shaped with respect to $a$ , and every filled triangle in it is among the triangles covered by the assumed condition and [L1].

1.2L1L4

For the holomorphy-to-vanishing-integrals direction, if $f$ is holomorphic on $Ω$ , [L4] gives zero integral around every filled triangle of [L1] contained in $Ω$ , including those with repeated or collinear vertices.

2.1step 1.1L2

For the vanishing-integrals-to-holomorphy direction, [L2] applied on $D (a, r)$ supplies a holomorphic function $F$ there with $F^{'} = f$ .

3.1step 2.1L3

For the vanishing-integrals-to-holomorphy direction, [L3] makes the derivative $F^{'}$ holomorphic, so $f = F^{'}$ is holomorphic on $D (a, r)$ .

4.1step 1.1step 1.2step 3.1∎

If $Ω$ is nonempty, the point in step 1.1 was arbitrary, so step 3.1 proves holomorphy throughout $Ω$ under the integral condition, while step 1.2 proves the converse; if $Ω$ is empty, both directions are vacuous.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Cauchy estimates on a smaller concentric disc

Statement

Let $0 \leq r < R < S$ , let $f$ be holomorphic on $D (a, S)$ , and suppose $M \geq 0$ satisfies $∣ f (ζ) ∣ \leq M$ whenever $∣ ζ - a ∣ = R$ . If $n \in N$ and $∣ z - a ∣ \leq r$ , then

$∣ f^{(n)} (z) ∣ \leq \frac{n! R M}{(R - r)^{n + 1}} .$

Facts & Assumptions

Given: Reals $0 \leq r < R < S$ , a function $f$ holomorphic on $D (a, S)$ , a bound $M \geq 0$ on the radius- $R$ circle, a natural $n$ , and a point $z$ with $∣ z - a ∣ \leq r$ .

[L1]

Cauchy's higher-derivative formula on the radius- $R$ circle gives $f^{(n)} (z) = n! (2 π i)^{- 1} \int_{γ} f (ζ) / (ζ - z)^{n + 1} d ζ$ for $∣ z - a ∣ < R < S$ (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).

[L2]

Complex modulus is multiplicative and satisfies the triangle inequality (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L3]

If an integrand has modulus at most $B$ on a rectifiable contour $γ$ , then the modulus of its integral is at most $B L (γ)$ (ML estimate: a contour integral is bounded by a supremum bound times path length).

[L4]

A once-traversed circle of radius $R > 0$ has length $2 π R$ (Every circle has circumference 2 pi r and circumference-to-diameter ratio pi).

Proof

technique · direct

1.1L1L2

Formula [L1] applies because $∣ z - a ∣ \leq r < R$ , and for $∣ ζ - a ∣ = R$ the triangle inequality in [L2] gives $∣ ζ - z ∣ \geq ∣ ζ - a ∣ - ∣ z - a ∣ \geq R - r > 0$ , so the integrand has modulus at most $M / (R - r)^{n + 1}$ .

2.1step 1.1L3L4algebra

Applying [L3] to step 1.1 and using the circle length from [L4] gives $∣ f^{(n)} (z) ∣ \leq (n! / (2 π)) (M / (R - r)^{n + 1}) (2 π R) = n! R M / (R - r)^{n + 1}$ .

3.1step 2.1∎

The bound in step 2.1 is independent of $z$ on the closed radius- $r$ disc and includes derivative order $n = 0$ , inner radius $r = 0$ , and bound $M = 0$ ; the strict inequality $r < R$ keeps every denominator positive.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly

Statement

Let $Ω \subseteq C$ be open, let each $f_{n} : Ω \to C$ be holomorphic, and suppose $f_{n} \to f$ locally uniformly on $Ω$ in the sense of Locally uniform convergence on an open subset of the complex plane is compact convergence. Then $f$ is holomorphic and

$f_{n}^{(k)} ⟶ f^{(k)}$

locally uniformly on $Ω$ for every natural $k$ , with $f^{(0)} = f$ .

A locally uniform limit of holomorphic functions is holomorphic, and for every natural $k$ the $k$ th derivatives converge locally uniformly to the $k$ th derivative of the limit.

Facts & Assumptions

Given: An open set $Ω$ , holomorphic functions $f_{n} : Ω \to C$ , and locally uniform convergence $f_{n} \to f$ , equivalently uniform convergence on every compact subset by Locally uniform convergence on an open subset of the complex plane is compact convergence.

[L1]

A uniform limit of continuous complex-valued functions on a metric space is continuous (A uniform limit of continuous complex-valued functions is continuous).

[L2]

Uniform convergence of continuous integrands on a fixed rectifiable contour permits passage of the limit through the complex line integral (A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral).

[L3]

Every holomorphic function has zero integral around each contained filled triangle, including degenerate triangles (Goursat's triangle theorem: a holomorphic function integrates to zero around every triangle contained in its domain).

[L4]

A continuous function on an open subset of $C$ is holomorphic if and only if its integral around every contained filled triangle is zero (Morera's theorem: vanishing triangle integrals characterize holomorphy among continuous functions).

[L5]

If $0 \leq r < R < S$ , $h$ is holomorphic on $D (a, S)$ , $M$ bounds $∣ h ∣$ on $∣ ζ - a ∣ = R$ , and $∣ z - a ∣ \leq r$ , then $∣ h^{(k)} (z) ∣ \leq k! R M / (R - r)^{k + 1}$ (Cauchy estimates on a smaller concentric disc).

[L6]

The boundary of a filled triangle is the union of its directed affine edge traces (Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter).

[L7]

Closed bounded subsets of Euclidean space, including $[0, 1]$ and closed complex discs, are compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L8]

The continuous image of a compact metric space is compact (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

Proof

technique · direct

1.1givenL1L7

If $Ω$ is nonempty, fix $a \in Ω$ and choose $S > 0$ with $\overline{D} (a, S) \subseteq Ω$ ; [L7] makes this closed disc compact, the given convergence is uniform there, and [L1] makes $f$ continuous on it, so $f$ is continuous throughout $Ω$ .

1.2givenL2L3L6L7L8

Let $Δ \subseteq Ω$ be any filled triangle. By [L6], its boundary trace is a finite union of affine images of $[0, 1]$ , compact by [L7] and [L8]; convergence is therefore uniform on the trace, [L3] makes every $\int_{\partial Δ} f_{n}$ zero, and [L2] gives $\int_{\partial Δ} f = 0$ .

2.1step 1.1step 1.2L4

The continuity from step 1.1 and the vanishing triangle integrals from step 1.2 satisfy [L4], so $f$ is holomorphic throughout $Ω$ ; on the empty open set this conclusion is vacuous.

3.1step 2.1choose

Fix a natural derivative order $k$ and a point $a \in Ω$ , and choose radii $0 < r < R < S$ with $\overline{D} (a, S) \subseteq Ω$ ; by step 2.1 every difference $h_{n} : = f_{n} - f$ is holomorphic on $D (a, S)$ .

4.1step 3.1L5

Given $ε > 0$ , uniform convergence on the compact circle $∣ ζ - a ∣ = R$ gives $N$ such that $∣ h_{n} (ζ) ∣ < ε (R - r)^{k + 1} / (k! R)$ there for $n \geq N$ ; applying [L5] then gives $∣ f_{n}^{(k)} (z) - f^{(k)} (z) ∣ < ε$ for every $∣ z - a ∣ \leq r$ .

5.1step 4.1∎

Step 4.1 proves uniform convergence of the $k$ th derivatives on a neighbourhood of every point, hence local uniform convergence by the dictionary in the given data; when $k = 0$ it recovers the original convergence, and zero or eventually constant sequences require no exception.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A locally uniformly convergent series of holomorphic functions may be differentiated term by term

Statement

Let $Ω \subseteq C$ be open and let $g_{j} : Ω \to C$ be holomorphic. Suppose the sequence of partial sums of $\sum_{j \geq 0} g_{j}$ converges locally uniformly to $g$ . Then $g$ is holomorphic, and for every natural $k$ ,

$g^{(k)} = \sum_{j \geq 0} g_{j}^{(k)},$

where the derivative series converges locally uniformly.

Facts & Assumptions

Given: Holomorphic functions $g_{j}$ on a common open set $Ω$ and locally uniform convergence of their complex-series partial sums as defined in Complex series, absolute convergence, complex power series, and radius of convergence.

[L1]

Complex differentiation is linear, and every constant function has derivative zero (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L2]

A locally uniform limit of holomorphic functions is holomorphic, and for every natural $k$ the $k$ th derivatives converge locally uniformly to the $k$ th derivative of the limit (Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).

Proof

technique · direct

1.1L1algebra

For the finite partial sum $S_{N} = \sum_{j < N} g_{j}$ , induction with [L1] gives $S_{N}^{(k)} = \sum_{j < N} g_{j}^{(k)}$ for every natural $k$ ; the empty partial sum is the zero holomorphic function.

2.1step 1.1L2

Apply [L2] to the locally uniformly convergent sequence $(S_{N})$ : its limit $g$ is holomorphic and $S_{N}^{(k)} \to g^{(k)}$ locally uniformly for every natural $k$ .

3.1step 1.1step 2.1∎

By step 1.1, the sequence in step 2.1 is exactly the partial-sum sequence of $\sum_{j \geq 0} g_{j}^{(k)}$ , proving the displayed termwise derivative formula; at $k = 0$ it is the original series.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

A jointly continuous finite-interval parameter integral of holomorphic functions is holomorphic

Statement

Let $a \leq b$ be real, let $Ω \subseteq C$ be open, and let $φ : [a, b] \times Ω \to C$ be jointly continuous. Suppose $φ (t, \cdot)$ is holomorphic on $Ω$ for every $t \in [a, b]$ . Then the componentwise Riemann integral

$F (z) : = \int_{a}^{b} φ (t, z) d t$

is holomorphic on $Ω$ .

If, in addition, $\partial_{z} φ (t, z)$ exists everywhere and is jointly continuous on $[a, b] \times Ω$ , then

$F^{'} (z) = \int_{a}^{b} \partial_{z} φ (t, z) d t .$

If $φ : [a, b] \times Ω \to C$ is jointly continuous and $φ (t, \cdot)$ is holomorphic for every $t$ , then $F (z) = \int_{a}^{b} φ (t, z) d t$ is holomorphic on $Ω$ .

Facts & Assumptions

Given: Real numbers $a \leq b$ , an open set $Ω \subseteq C$ , and a jointly continuous function $φ : [a, b] \times Ω \to C$ whose $z$ -slice is holomorphic for every parameter; the identification $C = R^{2}$ from $C$ is the real coordinate plane, with coordinate arithmetic.

[L1]

Complex-valued Riemann integration is the componentwise vector integral in $R^{2}$ , with zero integral when the limits agree and with linearity on every nondegenerate interval (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

On a piecewise- $C^{1}$ contour, the complex contour integral equals the sum of the parameter integrals of $f (γ (s)) γ^{'} (s)$ over its smooth pieces (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

[L3]

A Riemann-integrable real function on a product of nondegenerate closed rectangles has equal iterated integrals in either order when all sections are integrable (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections).

[L4]

A holomorphic function has zero integral around every contained filled triangle (Goursat's triangle theorem: a holomorphic function integrates to zero around every triangle contained in its domain).

[L5]

A continuous function with zero integral around every contained filled triangle is holomorphic (Morera's theorem: vanishing triangle integrals characterize holomorphy among continuous functions).

[L6]

If $H$ is a primitive of a continuous function $h$ on a neighbourhood of a rectifiable contour $γ$ , then $\int_{γ} h = H (γ (b)) - H (γ (a))$ (The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path).

[L7]

A continuous map on a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L8]

Closed bounded subsets of Euclidean space are compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L9]

Every continuous real function on a closed nondegenerate rectangle is Riemann integrable (Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable).

[L10]

Let $a \leq b$ . If $a < b$ and $h : [a, b] \to R^{m}$ is integrable, then $t \mapsto ∥ h (t) ∥_{2}$ is integrable, and in all cases $∥ \int_{a}^{b} h ∥_{2} \leq \int_{a}^{b} ∥ h ∥_{2}$ (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[L11]

If $q$ is Riemann integrable and $0 \leq q (t) \leq B$ on $[a, b]$ with $a < b$ , then $\int_{a}^{b} q (t) d t \leq B (b - a)$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

Proof

technique · direct

1.1givenL1L7L8L9L10L11

If $a = b$ , [L1] makes $F = 0$ , so all conclusions are immediate. Suppose $a < b$ . For each $z$ , continuity of $t \mapsto φ (t, z)$ and [L9] make the componentwise integral exist; near any fixed $z_{0}$ , choose a compactly contained closed disc $K$ , so [L8] makes $[a, b] \times K$ compact, [L7] makes $φ$ uniformly continuous there, and [L10] with [L11] gives $∥ F (z) - F (z_{0}) ∥_{2} \leq (b - a) \sup_{t \in [a, b]} ∣ φ (t, z) - φ (t, z_{0}) ∣ \to 0$ , hence $F$ is continuous.

1.2givenL2

For a filled triangle $Δ \subseteq Ω$ , parametrize each directed edge by its affine map on $[0, 1]$ ; [L2] rewrites the edge contribution to $\int_{\partial Δ} F (z) d z$ as an iterated parameter integral on $[a, b] \times [0, 1]$ .

1.3givenL2L6L7L8

For the differentiation-under-the-integral conclusion, now assume $ψ : = \partial_{z} φ$ exists and is jointly continuous. Fix $z \in Ω$ and a closed disc about $z$ contained in $Ω$ ; for sufficiently small nonzero $h$ , [L6] and the parametrization in [L2] on the segment from $z$ to $z + h$ give $(φ (t, z + h) - φ (t, z)) / h = \int_{0}^{1} ψ (t, z + s h) d s$ , and [L7] on the compact parameter-disc product from [L8] makes this quotient converge to $ψ (t, z)$ uniformly in $t$ .

2.1step 1.2L3L4L9

For the basic holomorphy conclusion, each real and imaginary component of the edge integrand in step 1.2 is continuous, hence Riemann integrable by [L9]; [L3] interchanges its parameter and edge integrals, and [L4] makes the resulting inner contour integral $\int_{\partial Δ} φ (t, z) d z$ zero for every fixed $t$ , so $\int_{\partial Δ} F (z) d z = 0$ .

3.1step 1.1step 2.1L5

For the basic holomorphy conclusion, the continuity from step 1.1 and the vanishing triangle integrals from step 2.1 satisfy [L5], so $F$ is holomorphic on $Ω$ .

4.1step 1.3L1L10L11∎

For the differentiation-under-the-integral conclusion, by linearity in [L1], the difference quotient of $F$ minus $\int_{a}^{b} ψ (t, z) d t$ is the integral over $t$ of the error in step 1.3; [L10] and [L11] bound its modulus by $(b - a)$ times the uniform error, which tends to zero, so $F^{'} (z) = \int_{a}^{b} \partial_{z} φ (t, z) d t$ , including the already settled case $a = b$ .

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

A holomorphic function equals its average on every circle inside a larger concentric holomorphy disc

Statement

Let $f$ be holomorphic on $D (a, R)$ and let $0 < r < R$ . Then

$f (a) = \frac{1}{2 π} \int_{0}^{2 π} f (a + r \exp (i θ)) d θ .$

Thus a holomorphic function equals its average on every positive-radius circle lying with a larger concentric disc inside its holomorphy domain.

Facts & Assumptions

Given: A function $f$ holomorphic on $D (a, R)$ and a radius $0 < r < R$ .

[L1]

Under these hypotheses, Cauchy's circle formula gives $f (z) = (2 π i)^{- 1} \int_{γ} f (ζ) / (ζ - z) d ζ$ for $∣ z - a ∣ < r$ , where $γ (θ) = a + r \exp (i θ)$ is positively oriented (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[L2]

For a piecewise- $C^{1}$ contour and an integrand continuous on its trace, the complex contour integral equals the parameter integral of the pulled-back integrand multiplied by the contour derivative (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

[L3]

Every holomorphic function is continuous (Complex differentiability at a point implies continuity there).

Proof

technique · direct

1.1L1

Apply [L1] at the centre $z = a$ to obtain $f (a) = (2 π i)^{- 1} \int_{γ} f (ζ) / (ζ - a) d ζ$ .

2.1step 1.1L2L3algebra

By [L3], $f$ is continuous; on the circle the denominator $ζ - a$ is nonzero because its modulus is $r > 0$ , so elementary complex division makes $ζ \mapsto f (ζ) / (ζ - a)$ continuous on the trace. With $ζ = γ (θ) = a + r \exp (i θ)$ , [L2] gives $d ζ = i r \exp (i θ) d θ$ while $ζ - a = r \exp (i θ)$ , so step 1.1 becomes $f (a) = (2 π i)^{- 1} \int_{0}^{2 π} f (a + r \exp (i θ)) i d θ$ .

3.1step 2.1algebra∎

Cancelling the nonzero factor $i$ in step 2.1 yields the stated circular average; the calculation requires $r > 0$ and also covers every constant or zero function.

CorollaryStatement: AI-generatedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Every nonconstant entire function has dense image in the complex plane

Statement

Every nonconstant entire function has dense image in the complex plane.

Equivalently, if $f : C \to C$ is entire and nonconstant, then every nonempty open disc meets $f [C]$ .

Facts & Assumptions

Given: A nonconstant entire function $f$ and the usual metric topology on $C$ from The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane.

[L1]

A subset of a topological space is dense exactly when it meets every nonempty open set, equivalently every nonempty member of a chosen basis (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets).

[L2]

If a complex differentiable function is nonzero at a point, its reciprocal is complex differentiable there; linear combinations of complex differentiable functions are complex differentiable (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L3]

Every bounded entire function is constant (Liouville's theorem: every bounded entire function is constant).

Proof

technique · direct

1.1givenL1choose

Suppose the image of $f$ is not dense. By [L1], some nonempty open set misses it; choosing a point $w$ of that set and a metric ball contained in it gives $ε > 0$ with $D (w, ε) \cap f [C] = \emptyset$ .

2.1step 1.1L2algebra

The function $f - w$ never vanishes, so [L2] makes $g : = 1 / (f - w)$ entire, and step 1.1 gives $∣ f (z) - w ∣ \geq ε$ and hence $∣ g (z) ∣ \leq 1 / ε$ for every $z$ .

3.1step 2.1L3

By step 2.1, $g$ is a bounded entire function, so [L3] makes it constant.

4.1step 3.1algebra∎

The constant $g$ is nonzero, and $f = w + 1 / g$ is therefore constant, contradicting the given hypothesis; thus the image is dense.

5 · Examples, counterexamples and false statements

None yet.