Session-authored (Fable 5 assisted)

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.

✓ 23 results · all verified · 14 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 9 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Complex Differentiability and the Cauchy–Riemann Equations

1 · Prerequisites

2 · Summary

The quotient construction of the complex numbers and their real-coordinate-plane model supply the arithmetic and Euclidean dictionary used here. Complex modulus gives the metric and topology, while real total derivatives, Jacobian matrices, the chain rule, and the continuous-partials criterion provide the multivariable differentiability results. The real exponential and trigonometric derivative formulas support the corresponding calculation for the complex exponential, and equality of mixed partials supplies the second-order input.

The development defines complex domains, complex differentiability, holomorphy, Wirtinger derivatives, antiholomorphy, and pointwise oriented conformality. It proves that complex differentiability is equivalent to real total differentiability together with a complex-linear real derivative, with a vanishing barred Wirtinger derivative, or with the Cauchy–Riemann equations; then derives derivative rules, a conditional inverse rule, polynomial and exponential examples, and constancy from a zero derivative on a domain. The final results connect nonzero derivatives with conformality and Jacobians, and show under explicit $C^{2}$ hypotheses that holomorphic components are harmonic, the derivative is holomorphic, and nondegenerate component critical points are saddles.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

$C = R [x] / (x^{2} + 1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves

The complex field used here is the quotient $C = R [x] / (x^{2} + 1)$ of The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ , with $i$ the class of $x$ . The bijection $Φ (a + b i) = (a, b)$ of $C$ is the real coordinate plane, with coordinate arithmetic carries addition and real scalar multiplication to the coordinatewise operations on $R^{2}$ , while complex multiplication becomes

$(a, b) (u, v) = (a u - b v, a v + b u) .$

Thus $C$ is the Euclidean plane as a real vector space, together with the additional bilinear operation of complex multiplication. A general real-linear map of the plane need not respect that operation and therefore need not be complex-linear.

The definitions in Real and imaginary parts, complex conjugation, and modulus make conjugation the reflection $(a, b) \mapsto (a, - b)$ and give $∣ a + b i ∣ = \sqrt{a^{2} + b^{2}}$ . In particular

$∣ z - w ∣ = ∥ Φ (z) - Φ (w) ∥_{2},$

so the metric, convergence, Cauchy, and continuity notions of The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane are exactly their Euclidean-plane counterparts. The metric topology is consequently the usual topology on $R^{2}$ , in accordance with The product, Euclidean-metric and norm topologies on $R^{n}$ agree, and for $n = 1$ they agree with the real-line topology. Openness, connectedness, and real total differentiability will always be read through this identification.

The identification supplies no compatible field order. Indeed $i^{2} = - 1$ , while in any ordered field a square is nonnegative and $1$ is positive. This obstruction concerns the multiplication, not the Euclidean geometry: the plane still has its inner product and orientation, but neither orders $C$ as a field.

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

A complex domain is a nonempty connected open subset of $C$

Definition

A complex domain is a nonempty, connected, open subset $U \subseteq C$ . Open means open in the modulus metric of The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, and connected has the meaning of Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets. By $C = R [x] / (x^{2} + 1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves, these are exactly the usual Euclidean notions for the corresponding subset of $R^{2}$ .

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

Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions

Definition

Let $U \subseteq C$ be open, let $a \in U$ , and let $f : U \to C$ . The function $f$ is complex differentiable at $a$ if the limit

$\lim_{\begin{array}{c} h \to 0 \\ h \neq 0, a + h \in U \end{array}} \frac{f (a + h) - f (a)}{h}$

exists in the metric of The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane. Its value is the complex derivative of $f$ at $a$ , denoted $f^{'} (a)$ . The increments are nonzero and remain in the domain; because $U$ is open, all sufficiently small increments are allowed.

The function $f$ is holomorphic on $U$ when it is complex differentiable at every point of $U$ . A function holomorphic on all of $C$ is entire. The word analytic is reserved for the local power-series notion.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

The complex derivative at a point is unique

Statement

If the complex derivative of $f : U \to C$ at $a \in U$ exists, its value is unique.

Facts & Assumptions

Given: An open set $U \subseteq C$ , a point $a \in U$ , and two complex numbers $L, M$ to which the difference quotient $(f (a + h) - f (a)) / h$ converges as $h \to 0$ through nonzero increments with $a + h \in U$ .

[F1]

Complex differentiability at $a$ means that the limit of $(f (a + h) - f (a)) / h$ exists as $h \to 0$ through nonzero increments with $a + h \in U$ (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

[L1]

For every $z, w \in C$ , $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ , and $∣ z ∣ = 0$ if and only if $z = 0$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $L \neq M$ , and put $ε = ∣ L - M ∣ / 3 > 0$ .

assume-contraL1

1.2

By the two asserted limits, choose $δ > 0$ such that every allowed $h$ with $0 < ∣ h ∣ < δ$ satisfies both $∣ q (h) - L ∣ < ε$ and $∣ q (h) - M ∣ < ε$ , where $q (h) = (f (a + h) - f (a)) / h$ .

givenF1choose

1.3

Since $U$ is open at $a$ , choose a nonzero allowed increment $h$ with $∣ h ∣ < δ$ .

givenchoose

2.1

The triangle inequality gives $∣ L - M ∣ \leq ∣ L - q (h) ∣ + ∣ q (h) - M ∣ < 2 ε = 2 ∣ L - M ∣ / 3$ , a contradiction. Hence $L = M$ .

step 1.1step 1.2step 1.3L1algebradischarge-contradiction∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-13Open item page →

The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions

Definition

Let $U \subseteq C$ be open and write a map $f : U \to C$ as $f = u + i v$ in Euclidean coordinates. At a point where the four real partial derivatives exist, define

$\partial_{z} f : = \frac{1}{2} (\partial_{x} f - i \partial_{y} f) = \frac{1}{2} (u_{x} + v_{y}) + \frac{i}{2} (v_{x} - u_{y}),$

$\partial_{\overset{ˉ}{z}} f : = \frac{1}{2} (\partial_{x} f + i \partial_{y} f) = \frac{1}{2} (u_{x} - v_{y}) + \frac{i}{2} (v_{x} + u_{y}) .$

The partial derivatives are those of Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ . If $f$ is real totally differentiable at the point, direct expansion gives the differential identity

$D f (h) = (\partial_{z} f) h + (\partial_{\overset{ˉ}{z}} f) \overline{h} .$

A real-differentiable map is antiholomorphic on $U$ when $\partial_{z} f = 0$ at every point of $U$ . Thus its differential is conjugate-linear at every point; no complex differentiability is asserted unless the other Wirtinger derivative also vanishes.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

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

Statement

Let $U \subseteq C$ be open, let $a \in U$ , and write $f = u + i v : U \to C$ . The following are equivalent:

$f$ is complex differentiable at $a$ .
Under $C ≅ R^{2}$ , the map $f$ is real totally differentiable at $a$ and $D f (a)$ is multiplication by a complex number.
The map $f$ is real totally differentiable at $a$ and $\partial_{\overset{ˉ}{z}} f (a) = 0$ .
The map $f$ is real totally differentiable at $a$ and satisfies the Cauchy–Riemann equations

$u_{x} (a) = v_{y} (a), u_{y} (a) = - v_{x} (a) .$

When these conditions hold,

$f^{'} (a) = u_{x} (a) + i v_{x} (a) = v_{y} (a) - i u_{y} (a) = \partial_{z} f (a) .$

Facts & Assumptions

Given: An open set $U \subseteq C$ , a point $a \in U$ , and a map $f = u + i v : U \to C$ .

[F1]

Complex differentiability at $a$ is existence of the limit $(f (a + h) - f (a)) / h$ as $h \to 0$ through nonzero increments with $a + h \in U$ (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

[F2]

Real total differentiability at $a$ means that for some real-linear $L$ , $f (a + h) = f (a) + L h + r (h)$ with $∥ r (h) ∥_{2} / ∥ h ∥_{2} \to 0$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, A linear map $L : R^{m} \to R^{n}$ in Euclidean coordinates).

[L1]

If a map is totally differentiable at $a$ , then its directional derivatives exist and equal $D f (a) v$ ; its partial derivatives are the columns of its Jacobian matrix (A total derivative computes every directional derivative, and its matrix is the Jacobian, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[L2]

Every real-linear map between Euclidean spaces has a unique matrix and is bounded by a constant times the Euclidean norm (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ ).

[L3]

Under $Φ (a + b i) = (a, b)$ , complex multiplication satisfies $(a + b i) (x + i y) = (a x - b y) + i (b x + a y)$ ( $C$ is the real coordinate plane, with coordinate arithmetic).

[F3]

For a real-differentiable $f$ , $D f (h) = (\partial_{z} f) h + (\partial_{\overset{ˉ}{z}} f) \overset{ˉ}{h}$ , with $\partial_{\overset{ˉ}{z}} f = \frac{1}{2} (u_{x} - v_{y}) + \frac{i}{2} (v_{x} + u_{y})$ (The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions).

[L4]

For complex numbers, $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z ∣ = 0$ if and only if $z = 0$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Proof

technique · direct

1.1

Assume condition 1 and write $L = f^{'} (a)$ . For $h \neq 0$ put $r (h) = f (a + h) - f (a) - L h$ ; then $∣ r (h) ∣ / ∣ h ∣ = ∣ (f (a + h) - f (a)) / h - L ∣ \to 0$ .

F1L4givenalgebra

1.2

Conversely assume condition 2, so $f (a + h) - f (a) = L h + r (h)$ with $∣ r (h) ∣ / ∣ h ∣ \to 0$ . For nonzero $h$ , division by $h$ gives $(f (a + h) - f (a)) / h = L + r (h) / h$ , and $∣ r (h) / h ∣ = ∣ r (h) ∣ / ∣ h ∣ \to 0$ ; hence condition 1 holds with $f^{'} (a) = L$ .

F1F2L4givenalgebra

1.3

Write the matrix of $D f (a)$ as $(\begin{array}{cc} u_{x} & u_{y} \\ v_{x} & v_{y} \end{array})$ by [L1]. By [L3], it is multiplication by $α + i β$ exactly when it is $(\begin{array}{cc} α & - β \\ β & α \end{array})$ .

L1L2L3

1.4

By [F3], $\partial_{\overset{ˉ}{z}} f (a) = 0$ exactly when both $u_{x} - v_{y} = 0$ and $v_{x} + u_{y} = 0$ . Hence condition 3 is equivalent to condition 4.

F3algebra

2.1

The map $h \mapsto L h$ is real-linear by the coordinate formula [L3], so step 1.1 is the remainder condition [F2]. Thus condition 2 holds.

step 1.1F2L2L3

2.2

Therefore condition 2 is equivalent to condition 4: equality with the multiplication matrix is exactly $u_{x} = v_{y}$ and $u_{y} = - v_{x}$ . In that case $α = u_{x} = v_{y}$ , $β = v_{x} = - u_{y}$ , so the multiplier is $u_{x} + i v_{x} = v_{y} - i u_{y}$ .

step 1.3algebra

3.1

Under the equivalent conditions, [F3] and the Cauchy–Riemann equations give $\partial_{z} f (a) = u_{x} + i v_{x}$ , while steps 1.2 and 2.2 identify the same number with $f^{'} (a)$ . Thus all four conditions are equivalent and the displayed derivative formulas hold.

step 1.2step 2.2step 1.4F3∎

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

Complex differentiability at a point implies continuity there

Statement

If $f : U \to C$ is complex differentiable at $a \in U$ , then $f$ is continuous at $a$ .

Facts & Assumptions

Given: An open set $U \subseteq C$ , a point $a \in U$ , and a function $f : U \to C$ complex differentiable at $a$ .

[L1]

Complex differentiability at $a$ is equivalent to real total differentiability there with derivative given by multiplication by a complex number (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).

[L2]

If a Euclidean map is totally differentiable at a point, then it is continuous there (Total differentiability gives a local $O (∥ h ∥_{2})$ increment bound and therefore continuity).

[F1]

Under $C = R^{2}$ , the modulus metric is exactly the Euclidean metric, and continuity on subsets of $C$ is metric continuity for this metric (The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane).

Proof

technique · direct

1.1

By [L1], $f$ is real totally differentiable at $a$ under the Euclidean identification.

givenL1

2.1

By [L2], the coordinate map is continuous at $a$ ; [F1] identifies this with continuity in the complex modulus metric.

step 1.1L2F1∎

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

Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set

Statement

Let $U \subseteq C$ be open, let $a \in U$ , and write $f = u + i v : U \to C$ . Suppose the four first partial derivatives of $u$ and $v$ exist on a neighbourhood of $a$ , are continuous at $a$ , and satisfy

$u_{x} (a) = v_{y} (a), u_{y} (a) = - v_{x} (a) .$

Then $f$ is complex differentiable at $a$ . Consequently, if these hypotheses hold at every point of $U$ , then $f$ is holomorphic on $U$ .

Facts & Assumptions

Given: The open set, point, function, partial-derivative hypotheses, and Cauchy–Riemann equations stated above.

[L1]

If every partial derivative of a Euclidean map exists on a neighbourhood of a point and is continuous at that point, then the map is totally differentiable there with derivative matrix equal to its Jacobian (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L2]

Real total differentiability together with the Cauchy–Riemann equations is equivalent to complex differentiability (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).

Proof

technique · direct

1.1

Apply [L1] to the coordinate map $(u, v)$ : it is real totally differentiable at $a$ .

givenL1

2.1

The assumed Cauchy–Riemann equations and [L2] now give complex differentiability at $a$ .

step 1.1givenL2

3.1

If the hypotheses hold at every point of $U$ , step 2.1 applies at every point, which is precisely holomorphy on $U$ .

step 2.1∎

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

Cartesian and polar forms of the Cauchy–Riemann equations agree away from the origin

Statement

Let $f = u + i v$ be real totally differentiable on an open subset of $C$ . On an open set of parameters $(r, θ)$ with $r > 0$ and $r e^{i θ}$ in the domain, put

$U (r, θ) = u (r \cos θ, r \sin θ), V (r, θ) = v (r \cos θ, r \sin θ) .$

At every such parameter point, the Cartesian Cauchy–Riemann equations are equivalent to

$U_{r} = \frac{1}{r} V_{θ}, V_{r} = - \frac{1}{r} U_{θ} .$

When these conditions hold,

$f^{'} (r e^{i θ}) = e^{- i θ} (U_{r} + i V_{r}) .$

No assertion is made at $r = 0$ , and no global choice of argument is used.

Facts & Assumptions

Given: A real totally differentiable $f = u + i v$ , a parameter point $(r, θ)$ with $r > 0$ , and the polar pullbacks $U, V$ stated above.

[L1]

The real total-derivative chain rule is $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L2]

The real derivatives satisfy $(\sin x)^{'} = \cos x$ and $(\cos x)^{'} = - \sin x$ (The derivatives of sine and cosine are cosine and minus sine).

[F1]

For real $x, y$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ ; in particular $e^{i θ} = \cos θ + i \sin θ$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L3]

For a real-differentiable complex-valued map, complex differentiability is equivalent to the Cartesian Cauchy–Riemann equations, and then $f^{'} = u_{x} + i v_{x}$ (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).

Proof

technique · direct

1.1

Put $c = \cos θ$ and $s = \sin θ$ . By [L1] and [L2], $U_{r} = u_{x} c + u_{y} s$ and $U_{θ} = r (- u_{x} s + u_{y} c)$ .

givenL1L2

1.2

The same calculation gives $V_{r} = v_{x} c + v_{y} s$ and $V_{θ} = r (- v_{x} s + v_{y} c)$ .

givenL1L2

2.1

If $u_{x} = v_{y}$ and $u_{y} = - v_{x}$ , steps 1.1–1.2 give $V_{θ} = r U_{r}$ and $U_{θ} = - r V_{r}$ , which are the polar equations because $r > 0$ .

step 1.1step 1.2algebra

2.2

Conversely, the inverse coordinate formulas are $u_{x} = U_{r} c - (U_{θ} / r) s$ , $u_{y} = U_{r} s + (U_{θ} / r) c$ , $v_{x} = V_{r} c - (V_{θ} / r) s$ , and $v_{y} = V_{r} s + (V_{θ} / r) c$ . Substituting the polar equations gives $u_{x} = v_{y}$ and $u_{y} = - v_{x}$ .

step 1.1step 1.2givenalgebra

3.1

Under either equivalent form, [L3] and step 2.2 give $f^{'} = u_{x} + i v_{x} = (c - i s) (U_{r} + i V_{r}) = e^{- i θ} (U_{r} + i V_{r})$ by [F1].

step 2.2L3F1algebra∎

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

Linearity, product, reciprocal, and quotient rules for complex derivatives

Statement

Let $f, g : U \to C$ be complex differentiable at $a \in U$ , and let $α, β \in C$ . Then

$(α f + β g)^{'} (a) = α f^{'} (a) + β g^{'} (a),$

$(f g)^{'} (a) = f^{'} (a) g (a) + f (a) g^{'} (a) .$

If $g (a) \neq 0$ , then $g$ is nonzero on some neighbourhood of $a$ , the reciprocal $1 / g$ is complex differentiable at $a$ , and

$(1 / g)^{'} (a) = - \frac{g^{'} (a)}{g (a)^{2}}, (f / g)^{'} (a) = \frac{f^{'} (a) g (a) - f (a) g^{'} (a)}{g (a)^{2}} .$

Every constant function has derivative $0$ , and the identity function has derivative $1$ .

Facts & Assumptions

Given: An open set $U \subseteq C$ , a point $a \in U$ , functions $f, g : U \to C$ complex differentiable at $a$ , and scalars $α, β \in C$ .

[F1]

Complex differentiability at $a$ is existence of the difference-quotient limit at $a$ (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

[L1]

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

[L2]

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

Proof

technique · direct

1.1

The difference quotients of a constant function and of the identity are respectively $0$ and $1$ , so their derivatives have those values.

F1algebra

1.2

Taking the finite linear combination of the two difference quotients gives $(α f + β g)^{'} (a) = α f^{'} (a) + β g^{'} (a)$ .

givenF1algebra

1.3

For nonzero allowed $h$ , $\frac{f (a + h) g (a + h) - f (a) g (a)}{h} = f (a + h) \frac{g (a + h) - g (a)}{h} + g (a) \frac{f (a + h) - f (a)}{h} .$

algebra

1.4

Suppose $g (a) \neq 0$ . Continuity [L1] supplies a neighbourhood of $a$ on which $∣ g (z) - g (a) ∣ < ∣ g (a) ∣$ , and on this neighbourhood $g (z) \neq 0$ by [L2].

givenL1L2

2.1

By [L1], $f (a + h) \to f (a)$ , while the two quotients in step 1.3 tend to $g^{'} (a)$ and $f^{'} (a)$ ; hence the product formula follows.

step 1.3givenF1L1algebra

2.2

For nonzero allowed $h$ in that neighbourhood, $\frac{g (a + h)^{- 1} - g (a)^{- 1}}{h} = - \frac{1}{g (a + h) g (a)} \frac{g (a + h) - g (a)}{h} .$

step 1.4algebra

3.1

The reciprocal factor in step 2.2 tends to $1 / g (a)^{2}$ , so the reciprocal derivative is $- g^{'} (a) / g (a)^{2}$ . Applying the product rule to $f (1 / g)$ and simplifying gives the quotient formula.

step 2.1step 2.2givenF1L2algebra∎

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

The chain rule for complex derivatives

Statement

Let $f : U \to V$ and $g : V \to C$ , where $U, V \subseteq C$ are open. If $f$ is complex differentiable at $a \in U$ and $g$ is complex differentiable at $f (a)$ , then $g \circ f$ is complex differentiable at $a$ and

$(g \circ f)^{'} (a) = g^{'} (f (a)) f^{'} (a) .$

Facts & Assumptions

Given: The maps, domains, point, and differentiability hypotheses in the Statement.

[L1]

Complex differentiability at a point is equivalent to real total differentiability with total derivative given by multiplication by the complex derivative (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).

[L2]

If $f$ is totally differentiable at $a$ and $g$ is totally differentiable at $f (a)$ , then $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

Proof

technique · direct

1.1

By [L1], $D f (a)$ is multiplication by $f^{'} (a)$ and $D g (f (a))$ is multiplication by $g^{'} (f (a))$ .

givenL1

2.1

By [L2], $g \circ f$ is real totally differentiable and its derivative is the composite of the maps in step 1.1, namely multiplication by $g^{'} (f (a)) f^{'} (a)$ .

step 1.1L2algebra

3.1

Applying the reverse implication of [L1] gives complex differentiability of $g \circ f$ and the asserted derivative.

step 2.1L1∎

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

The Wirtinger chain rule for compositions of real-differentiable complex-valued maps

Statement

Let $f : U \to V$ and $g : V \to C$ , where $U, V \subseteq C$ are open, and suppose $f$ is real totally differentiable at $a \in U$ and $g$ is real totally differentiable at $f (a)$ . Writing the Wirtinger variables of $g$ as $w, \overset{ˉ}{w}$ , one has

$(g \circ f)_{z} = (g_{w} \circ f) f_{z} + (g_{\overset{ˉ}{w}} \circ f) \overline{f_{\overset{ˉ}{z}}},$

$(g \circ f)_{\overset{ˉ}{z}} = (g_{w} \circ f) f_{\overset{ˉ}{z}} + (g_{\overset{ˉ}{w}} \circ f) \overline{f_{z}}$

at $a$ . If both maps are holomorphic, these formulas reduce to the complex chain rule.

Facts & Assumptions

Given: The maps, domains, point, and real total-differentiability hypotheses in the Statement.

[F1]

For a real-differentiable complex-valued map, $D f (h) = f_{z} h + f_{\overset{ˉ}{z}} \overset{ˉ}{h}$ (The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions).

[L1]

The total derivative of a composite is the composite of the total derivatives (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L2]

Complex conjugation satisfies $\overline{z + w} = \overset{ˉ}{z} + \overset{ˉ}{w}$ and $\overline{z w} = \overset{ˉ}{z} \overset{ˉ}{w}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Proof

technique · direct

1.1

Put $A = f_{z} (a)$ , $B = f_{\overset{ˉ}{z}} (a)$ , $C = g_{w} (f (a))$ , and $D = g_{\overset{ˉ}{w}} (f (a))$ . By [F1], $D f (a) h = A h + B \overset{ˉ}{h}$ and $D g (f (a)) k = C k + D \overset{ˉ}{k}$ .

givenF1

1.2

For the identity inner map, $(A, B) = (1, 0)$ and the two asserted coefficients reduce to $(C, D)$ . For conjugation, $(A, B) = (0, 1)$ and they become $(D, C)$ , as direct substitution $g (\overset{ˉ}{z})$ requires. For a constant inner map, $A = B = 0$ and both coefficients vanish.

F1L2algebra

2.1

By [L1] and [L2], $D (g \circ f) (a) h = (C A + D \overset{ˉ}{B}) h + (C B + D \overset{ˉ}{A}) \overset{ˉ}{h} .$

step 1.1L1L2algebra

3.1

Comparing step 2.1 with the unique Wirtinger expansion [F1] gives the two displayed formulas. For holomorphic $f, g$ , the barred coefficients vanish, leaving $(g \circ f)_{z} = (g_{w} \circ f) f_{z}$ .

step 2.1F1algebra∎

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

A conjugate difference quotient characterizes antiholomorphic maps

Statement

Let $U \subseteq C$ be open, let $a \in U$ , and let $f : U \to C$ . The limit

$G = \lim_{\begin{array}{c} h \to 0 \\ h \neq 0 \end{array}} \frac{f (a + h) - f (a)}{\overset{ˉ}{h}}$

exists if and only if $f$ is real totally differentiable at $a$ and $f_{z} (a) = 0$ . In that case $f_{\overset{ˉ}{z}} (a) = G$ . Consequently, the conjugate quotient exists at every point of $U$ exactly for real-differentiable antiholomorphic maps, and its value is $f_{\overset{ˉ}{z}}$ .

Facts & Assumptions

Given: An open set $U \subseteq C$ , a point $a \in U$ , and a map $f : U \to C$ .

[F1]

Total differentiability at $a$ means $f (a + h) = f (a) + D f (a) h + r (h)$ with $∣ r (h) ∣ / ∣ h ∣ \to 0$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[F2]

For a real-differentiable map, $D f (a) h = f_{z} (a) h + f_{\overset{ˉ}{z}} (a) \overset{ˉ}{h}$ (The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions).

[L1]

Every real-linear map between Euclidean spaces has a matrix and is bounded by a constant times the Euclidean norm (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ ).

[L2]

Conjugation is a real-field automorphism with $\overline{\overline{z}} = z$ , the modulus is multiplicative, and $z \overline{z} = ∣ z ∣^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive). Since $\overline{\overline{z}} = z$ and $z \overline{z} = ∣ z ∣^{2}$ , one has $∣ \overline{z} ∣^{2} = \overline{z} \overline{\overline{z}} = \overline{z} z = ∣ z ∣^{2}$ , and both moduli are nonnegative, so $∣ \overline{z} ∣ = ∣ z ∣$ , so in particular $∣ \overset{ˉ}{h} ∣ = ∣ h ∣$ .

Proof

technique · direct

1.1

Suppose the conjugate quotient tends to $G$ , and put $r (h) = f (a + h) - f (a) - G \overset{ˉ}{h}$ . Then $∣ r (h) ∣ / ∣ h ∣ = ∣ (f (a + h) - f (a)) / \overset{ˉ}{h} - G ∣ \to 0$ .

givenL2algebra

1.2

Conversely, suppose $f$ is real totally differentiable and $f_{z} (a) = 0$ . By [F1] and [F2], $f (a + h) - f (a) = f_{\overset{ˉ}{z}} (a) \overset{ˉ}{h} + r (h)$ with $∣ r (h) ∣ / ∣ h ∣ \to 0$ .

givenF1F2

1.3

For the identity map, [F2] gives $f_{z} = 1$ and $f_{\overset{ˉ}{z}} = 0$ , while its conjugate quotient is $h / \overset{ˉ}{h}$ and has incompatible values $1$ and $- 1$ on real and imaginary increments. For conjugation, [F2] gives $f_{z} = 0$ and $f_{\overset{ˉ}{z}} = 1$ , and its conjugate quotient is identically $1$ . These two tests confirm the placement of the conjugates and the barred coefficient.

F2L2algebra

2.1

The map $h \mapsto G \overset{ˉ}{h}$ is real-linear and bounded by $∣ G ∣ ∣ h ∣$ , so [F1] and step 1.1 show that $f$ is real totally differentiable with $D f (a) h = G \overset{ˉ}{h}$ .

step 1.1F1L1L2

3.1

Comparing this differential with [F2] gives $f_{z} (a) = 0$ and $f_{\overset{ˉ}{z}} (a) = G$ .

step 2.1F2algebra

4.1

Dividing by $\overset{ˉ}{h}$ and using $∣ \overset{ˉ}{h} ∣ = ∣ h ∣$ gives $(f (a + h) - f (a)) / \overset{ˉ}{h} = f_{\overset{ˉ}{z}} (a) + r (h) / \overset{ˉ}{h} \to f_{\overset{ˉ}{z}} (a)$ . This proves the reverse implication and the value of the limit.

step 1.2L2algebra∎

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

A holomorphic function with continuous complex derivative has $C^{1}$ real and imaginary components

Statement

Let $f = u + i v$ be holomorphic on an open set $U \subseteq C$ . If $f^{'} : U \to C$ is continuous, then $u$ and $v$ are of class $C^{1}$ on $U$ .

Facts & Assumptions

Given: A holomorphic $f = u + i v$ on $U$ whose complex derivative $f^{'}$ is continuous.

[L1]

For a complex-differentiable map, $f^{'} = u_{x} + i v_{x} = v_{y} - i u_{y}$ (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).

[F1]

If $w = a + b i$ , then $Re w = a$ , $Im w = b$ , and $∣ w ∣ = \sqrt{a^{2} + b^{2}}$ (Real and imaginary parts, complex conjugation, and modulus).

Proof

technique · direct

1.1

By [L1], $u_{x} = Re f^{'}$ , $v_{x} = Im f^{'}$ , $u_{y} = - Im f^{'}$ , and $v_{y} = Re f^{'}$ throughout $U$ .

givenL1

1.2

From [F1], $∣ Re (w_{1} - w_{2}) ∣ \leq ∣ w_{1} - w_{2} ∣$ and $∣ Im (w_{1} - w_{2}) ∣ \leq ∣ w_{1} - w_{2} ∣$ , so the real and imaginary part maps are continuous.

F1algebra

2.1

Since $f^{'}$ is continuous, steps 1.1–1.2 show that all four first partial derivatives of $u$ and $v$ are continuous. Hence both components are $C^{1}$ .

step 1.1step 1.2given∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

A continuous local inverse has derivative reciprocal to a nonzero complex derivative

Statement

Let $U, V \subseteq C$ be open, let $f : U \to V$ be a bijection, and let $g = f^{- 1} : V \to U$ . Fix $a \in U$ and put $b = f (a)$ . If $f$ is complex differentiable at $a$ , $f^{'} (a) \neq 0$ , and $g$ is continuous at $b$ , then $g$ is complex differentiable at $b$ and

$g^{'} (b) = \frac{1}{f^{'} (a)} .$

The existence or continuity of such an inverse is a hypothesis, not a consequence of $f^{'} (a) \neq 0$ here.

Facts & Assumptions

Given: The open sets, bijection, inverse, points, differentiability, nonzero-derivative, and inverse-continuity hypotheses in the Statement.

[F1]

Complex differentiability at $a$ means $(f (a + h) - f (a)) / h \to f^{'} (a)$ through nonzero allowed increments (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

[L1]

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

Proof

technique · direct

1.1

For $w \neq b$ near $b$ , put $z = g (w)$ . Injectivity gives $z \neq a$ , and $\frac{g (w) - g (b)}{w - b} = \frac{z - a}{f (z) - f (a)} = {(\frac{f (z) - f (a)}{z - a})}^{- 1} .$

givenalgebra

2.1

As $w \to b$ , continuity of $g$ gives $z \to a$ . By [F1], the parenthesized quotient in step 1.1 tends to the nonzero number $f^{'} (a)$ .

step 1.1givenF1

3.1

If $q \to q_{0} \neq 0$ , then $q^{- 1} - q_{0}^{- 1} = (q_{0} - q) / (q q_{0}) \to 0$ , with denominators nonzero near the limit by [L1]. Applying this to step 2.1 proves $g^{'} (b) = 1 / f^{'} (a)$ .

step 2.1L1algebra∎

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

Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero

Statement

Let $P (z) = \sum_{k = 0}^{n} a_{k} z^{k}$ be a complex polynomial. Then $P$ is entire and

$P^{'} (z) = \sum_{k = 1}^{n} k a_{k} z^{k - 1} .$

This includes the zero polynomial and constant polynomials, whose derivative is zero. If $P, Q$ are complex polynomials, then the set $D = {z \in C : Q (z) \neq 0}$ is open, $P / Q$ is holomorphic on $D$ , and

$(P / Q)^{'} = \frac{P^{'} Q - P Q^{'}}{Q^{2}} .$

When $Q$ is a nonzero constant, $D = C$ ; when $Q$ is the zero polynomial, $D = \emptyset$ and no rational function is defined there.

Facts & Assumptions

Given: Complex polynomials $P, Q$ with finite coefficient support.

[L1]

Constants and the identity have derivatives $0$ and $1$ ; finite linear combinations, products, reciprocals, and quotients obey the displayed derivative rules wherever denominators are nonzero (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[F1]

A polynomial over a commutative ring is a finitely supported coefficient sequence, written formally as a finite sum $\sum_{i} a_{i} x^{i}$ (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L2]

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

[L3]

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

Proof

technique · direct

1.1

For $m \geq 1$ and $h \neq 0$ , the factorization $((z + h)^{m} - z^{m}) / h = \sum_{j = 0}^{m - 1} (z + h)^{m - 1 - j} z^{j}$ has limit $m z^{m - 1}$ ; for $m = 0$ the function is constant and has derivative $0$ by [L1].

L1algebra

2.1

By finite support [F1], $P$ is a finite linear combination of these powers. The linearity rule [L1] and step 1.1 make $P$ entire with the asserted derivative, including the empty-support zero polynomial.

step 1.1F1L1

3.1

Fix $z_{0} \in D$ . By step 2.1 and [L2], $Q$ is continuous at $z_{0}$ , so some neighbourhood satisfies $∣ Q (z) - Q (z_{0}) ∣ < ∣ Q (z_{0}) ∣$ ; [L3] then forces $Q (z) \neq 0$ . Thus $D$ is open.

step 2.1L2L3given

4.1

On $D$ , both polynomials are holomorphic and $Q$ is nonzero. The quotient rule [L1] gives the displayed derivative. If $Q$ is a nonzero constant then it never vanishes, while for $Q = 0$ the set $D$ is empty.

step 2.1step 3.1L1algebra∎

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

The complex exponential is entire and its complex derivative is itself

Statement

The complex exponential is entire, and

$\exp^{'} (z) = \exp z$

for every $z \in C$ .

Facts & Assumptions

Given: A complex number $z = x + i y$ and the published complex exponential.

[F1]

For real $x, y$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L1]

The real exponential is $C^{\infty}$ and $(e^{x})^{'} = e^{x}$ (The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[L2]

The real derivatives are $(\sin y)^{'} = \cos y$ and $(\cos y)^{'} = - \sin y$ (The derivatives of sine and cosine are cosine and minus sine).

[L3]

A real function differentiable at a point is continuous there (A function differentiable at $c$ is continuous at $c$ ).

[L4]

Finite sums and products of continuous real-valued maps on a topological space are continuous (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[L5]

Continuous first partial derivatives satisfying the Cauchy–Riemann equations give complex differentiability, and holomorphy when this holds at every point (Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set). Where $f$ is complex differentiable, $f^{'} = u_{x} + i v_{x}$ (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).

Proof

technique · direct

1.1

By [F1], the real and imaginary components are $u (x, y) = e^{x} \cos y$ and $v (x, y) = e^{x} \sin y$ .

givenF1

2.1

By [L1] and [L2], $u_{x} = e^{x} \cos y, u_{y} = - e^{x} \sin y, v_{x} = e^{x} \sin y, v_{y} = e^{x} \cos y .$

step 1.1L1L2algebra

3.1

The one-variable factors in step 2.1 are continuous by [L1]–[L3]; their pullbacks along the coordinate projections are continuous, and [L4] makes all four displayed partials continuous on $R^{2}$ .

step 2.1L1L2L3L4

4.1

Step 2.1 gives $u_{x} = v_{y}$ and $u_{y} = - v_{x}$ everywhere. By [L5], the complex exponential is entire and its derivative is $u_{x} + i v_{x} = e^{x} (\cos y + i \sin y) = \exp z$ .

step 1.1step 2.1step 3.1L5∎

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

A holomorphic function with zero derivative on a domain is constant

Statement

Let $U \subseteq C$ be a domain. If $f : U \to C$ is holomorphic and $f^{'} (z) = 0$ for every $z \in U$ , then $f$ is constant on $U$ .

Facts & Assumptions

Given: A complex domain $U$ and a holomorphic function $f : U \to C$ with $f^{'} = 0$ throughout $U$ .

[F1]

A complex domain is a nonempty connected open subset of $C$ (A complex domain is a nonempty connected open subset of $C$ ).

[L1]

For an open subset of $R^{n}$ , connectedness, path-connectedness, and polygonal connectedness are equivalent (For an open subset of $R^{n}$ , connectedness, path-connectedness and polygonal connectedness are equivalent).

[F2]

A polygonal path is a finite concatenation of affine line segments with consecutive vertices (Polygonal paths and polygonally connected subsets of $R^{n}$ ).

[L2]

If $f$ is complex differentiable at a point, then its real total derivative is multiplication by $f^{'}$ (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).

[L3]

The total derivative of a composite is the composite of the total derivatives (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L4]

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

[L5]

A real function continuous on an order-convex interval and differentiable at every interior point, with derivative zero there, is constant on that interval (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

Proof

technique · direct

1.1

Let $p, q \in U$ . By [F1] and [L1], choose a polygonal path in $U$ from $p$ to $q$ , with vertices $v_{0} = p, v_{1}, \dots, v_{m} = q$ as in [F2].

givenF1L1F2choose

2.1

For each segment put $γ_{j} (t) = (1 - t) v_{j - 1} + t v_{j}$ for $0 \leq t \leq 1$ . The composite $f \circ γ_{j}$ is continuous on $[0, 1]$ by [L4], including at the endpoints.

step 1.1L4

2.2

At every $t \in (0, 1)$ , [L2] makes $D f (γ_{j} (t))$ multiplication by $0$ , and [L3] therefore gives $D (f \circ γ_{j}) (t) = 0$ . Hence the real and imaginary components of $f \circ γ_{j}$ have derivative zero on $(0, 1)$ .

step 1.1givenL2L3algebra

3.1

By [L5], both components are constant on $[0, 1]$ , so $f (v_{j - 1}) = f (v_{j})$ for each segment, including a zero-length segment if one occurs.

step 2.1step 2.2L5

4.1

Chaining the finitely many equalities from step 3.1 gives $f (p) = f (q)$ . Since $p, q$ were arbitrary, $f$ is constant on the nonempty domain $U$ .

step 1.1step 3.1F1∎

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

A real-valued holomorphic function on a domain is constant

Statement

If $f : U \to C$ is holomorphic on a domain $U$ and $f (U) \subseteq R$ , then $f$ is constant.

Facts & Assumptions

Given: A domain $U$ and a holomorphic $f = u + i v : U \to C$ with $v = 0$ .

[L1]

A holomorphic map satisfies $u_{x} = v_{y}$ , $u_{y} = - v_{x}$ , and $f^{'} = u_{x} + i v_{x}$ (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).

[L2]

A holomorphic function with zero derivative on a domain is constant (A holomorphic function with zero derivative on a domain is constant).

Proof

technique · direct

1.1

Since $v = 0$ , both $v_{x}$ and $v_{y}$ vanish. The Cauchy–Riemann equations [L1] then give $u_{x} = u_{y} = 0$ , so $f^{'} = 0$ throughout $U$ .

givenL1algebra

2.1

Apply [L2] to conclude that $f$ is constant on $U$ .

step 1.1L2∎

CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-13Open item page →

A holomorphic function of constant modulus on a domain is constant

Statement

Let $U$ be a complex domain and let $f : U \to C$ be holomorphic. If $∣ f ∣$ is constant on $U$ , then $f$ is constant.

Facts & Assumptions

Given: A domain $U$ , a holomorphic $f = u + i v$ on $U$ , and a real $c \geq 0$ with $∣ f (z) ∣ = c$ for every $z \in U$ .

[L1]

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

[L2]

[L3]

A holomorphic function with zero derivative on a domain is constant (A holomorphic function with zero derivative on a domain is constant).

Proof

technique · cases

1.1

Suppose first that $c = 0$ . Then $∣ f ∣ = 0$ , so $f = 0$ by [L1] and is constant.

assume-case zerogivenL1

1.2

Suppose next that $c > 0$ . Differentiating $u^{2} + v^{2} = c^{2}$ in the two real coordinates gives $u u_{x} + v v_{x} = 0$ and $u u_{y} + v v_{y} = 0$ .

assume-case posgivenL1algebra

2.1

Using [L2], the equations of step 1.2 become $u u_{x} - v u_{y} = 0$ and $v u_{x} + u u_{y} = 0$ . Their coefficient determinant is $u^{2} + v^{2} = c^{2} > 0$ , so $u_{x} = u_{y} = 0$ .

step 1.2L2algebra

3.1

Again by [L2], $v_{x} = - u_{y} = 0$ and $f^{'} = u_{x} + i v_{x} = 0$ throughout $U$ . Hence [L3] makes $f$ constant in the positive-modulus case.

step 2.1L2L3

4.1

The cases $c = 0$ and $c > 0$ exhaust $c \geq 0$ , and both give constancy.

step 1.1step 3.1cases-exhaustive∎

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

If both $f$ and $\overset{ˉ}{f}$ are holomorphic on a domain, then $f$ is constant

Statement

Let $U$ be a complex domain. If $f$ and $\overset{ˉ}{f}$ are both holomorphic on $U$ , then $f$ is constant.

Facts & Assumptions

Given: A domain $U$ and a function $f = u + i v$ such that both $f$ and $\overset{ˉ}{f} = u - i v$ are holomorphic on $U$ .

[L1]

A holomorphic map $p + i q$ satisfies $p_{x} = q_{y}$ and $p_{y} = - q_{x}$ , with derivative $p_{x} + i q_{x}$ (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).

[L2]

A holomorphic function with zero derivative on a domain is constant (A holomorphic function with zero derivative on a domain is constant).

Proof

technique · direct

1.1

Applying [L1] to $f$ gives $u_{x} = v_{y}$ and $u_{y} = - v_{x}$ , while applying it to $\overset{ˉ}{f} = u + i (- v)$ gives $u_{x} = - v_{y}$ and $u_{y} = v_{x}$ .

givenL1

2.1

The paired equations imply $u_{x} = u_{y} = v_{x} = v_{y} = 0$ , so [L1] gives $f^{'} = 0$ throughout $U$ .

step 1.1L1algebra

3.1

The domain theorem [L2] now makes $f$ constant.

step 2.1L2∎

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

Orientation-preserving conformality for a real-differentiable complex map at a point

Definition

For vectors $p = (p_{1}, p_{2})$ and $q = (q_{1}, q_{2})$ in the oriented Euclidean plane, put

$ω (p, q) : = p_{1} q_{2} - p_{2} q_{1} .$

A real-linear map $L : R^{2} \to R^{2}$ is a similarity of ratio $λ > 0$ when

$⟨ L h, L k ⟩ = λ^{2} ⟨ h, k ⟩$

for all $h, k \in R^{2}$ , using the inner product of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ . It is orientation-preserving when $ω (L e_{1}, L e_{2}) > 0$ and orientation-reversing when that quantity is negative.

Let $U \subseteq C$ be open and let $f : U \to C$ be real totally differentiable at $a$ . The map $f$ is orientation-preserving conformal at $a$ when $D f (a)$ is an orientation-preserving similarity. This is a pointwise condition on the real derivative. It asserts neither local nor global injectivity of $f$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Plane similarities are complex or conjugate-complex multiplications; the orientation-preserving ones are exactly the nonzero complex multiplications

Statement

Let $L : R^{2} \to R^{2}$ be real-linear. It is a similarity if and only if exactly one of the following forms holds for some $ξ \in C ∖ {0}$ :

$L h = ξ h, L h = ξ \overset{ˉ}{h} .$

The first form is orientation-preserving and the second orientation-reversing. Thus the orientation-preserving similarities are exactly the nonzero complex multiplications.

Facts & Assumptions

Given: A real-linear map $L : R^{2} \to R^{2}$ .

[F1]

A similarity has a ratio $λ > 0$ and satisfies $⟨ L h, L k ⟩ = λ^{2} ⟨ h, k ⟩$ ; its orientation is the sign of $ω (L e_{1}, L e_{2})$ (Orientation-preserving conformality for a real-differentiable complex map at a point).

[F2]

The Euclidean inner product is $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ and is positive definite (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L1]

Under $C ≅ R^{2}$ , multiplication satisfies $(a + b i) (x + i y) = (a x - b y) + i (b x + a y)$ ( $C$ is the real coordinate plane, with coordinate arithmetic).

Proof

technique · direct

1.1

Suppose $L$ is a similarity of ratio $λ$ , and write its columns as $p = L e_{1} = (a, b)$ and $q = L e_{2} = (c, d)$ . By [F1]–[F2], $p ⊥ q$ and $∣ p ∣ = ∣ q ∣ = λ > 0$ .

givenF1F2

1.2

Conversely, for $ξ = a + b i \neq 0$ , direct expansion using [F2] shows that both $h \mapsto ξ h$ and $h \mapsto ξ \overset{ˉ}{h}$ multiply every inner product by $∣ ξ ∣^{2}$ . Their signed area factors are respectively $∣ ξ ∣^{2}$ and $- ∣ ξ ∣^{2}$ , so both are similarities with the asserted orientations.

F1F2L1algebra

2.1

In the plane, a vector orthogonal to the nonzero $p = (a, b)$ and of the same length is either $(- b, a)$ or $(b, - a)$ . Hence $q$ is one of these two vectors.

step 1.1algebra

3.1

If $q = (- b, a)$ , [L1] gives $L h = (a + b i) h$ and $ω (p, q) = a^{2} + b^{2} > 0$ . If $q = (b, - a)$ , [L1] gives $L h = (a + b i) \overset{ˉ}{h}$ and $ω (p, q) = - (a^{2} + b^{2}) < 0$ .

step 2.1L1algebra

4.1

The signed area factor cannot be both positive and negative, so the two forms are mutually exclusive and the classification is complete.

step 3.1step 1.2algebra∎

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

A real-differentiable complex map is orientation-preserving conformal at a point exactly when it is complex differentiable there with nonzero derivative

Statement

Let $f : U \to C$ be real totally differentiable at $a \in U$ . Then $f$ is orientation-preserving conformal at $a$ if and only if it is complex differentiable at $a$ and $f^{'} (a) \neq 0$ .

Facts & Assumptions

Given: An open $U \subseteq C$ , a point $a \in U$ , and a map $f : U \to C$ real totally differentiable at $a$ .

[L1]

Complex differentiability at $a$ is equivalent to $D f (a)$ being multiplication by the complex derivative (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).

[F1]

Orientation-preserving conformality at $a$ means that $D f (a)$ is an orientation-preserving similarity (Orientation-preserving conformality for a real-differentiable complex map at a point).

[L2]

The orientation-preserving similarities of the plane are exactly the maps $h \mapsto ξ h$ with $ξ \neq 0$ (Plane similarities are complex or conjugate-complex multiplications; the orientation-preserving ones are exactly the nonzero complex multiplications).

Proof

technique · direct

1.1

If $f$ is complex differentiable at $a$ with $f^{'} (a) \neq 0$ , [L1] makes $D f (a)$ multiplication by $f^{'} (a)$ , and [L2] makes this an orientation-preserving similarity. Hence $f$ is conformal at $a$ by [F1].

givenL1L2F1

1.2

Conversely, if $f$ is orientation-preserving conformal at $a$ , [F1] and [L2] give $D f (a) h = ξ h$ for some $ξ \neq 0$ . The reverse direction of [L1] makes $f$ complex differentiable with $f^{'} (a) = ξ \neq 0$ .

givenF1L2L1

2.1

Steps 1.1 and 1.2 prove both directions of the equivalence.

step 1.1step 1.2∎

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

The Jacobian determinant of a holomorphic map is $∣ f^{'} ∣^{2}$ and is positive exactly where $f^{'} \neq 0$

Statement

Let $f = u + i v$ be holomorphic on an open set $U \subseteq C$ . At every $z \in U$ ,

$\det J f (z) = ∣ f^{'} (z) ∣^{2} \geq 0.$

The determinant is positive exactly where $f^{'} (z) \neq 0$ , and it is zero exactly where $f^{'} (z) = 0$ ; it is never negative.

Facts & Assumptions

Given: A holomorphic map $f = u + i v$ and a point $z$ in its open domain.

[L1]

If $f^{'} (z) = a + i b$ , then the real derivative matrix is $(\begin{array}{cc} a & - b \\ b & a \end{array})$ (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).

[F1]

The Jacobian matrix is the matrix of the first partial derivatives (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[L2]

Complex modulus satisfies $∣ a + i b ∣^{2} = a^{2} + b^{2}$ , and $∣ w ∣ = 0$ if and only if $w = 0$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Proof

technique · direct

1.1

By [L1] and [F1], $\det J f (z) = a^{2} + b^{2} = ∣ f^{'} (z) ∣^{2}$ .

givenL1F1L2algebra

2.1

The sum $a^{2} + b^{2}$ is nonnegative and, by [L2], is zero exactly when $f^{'} (z) = 0$ ; otherwise it is positive.

step 1.1L2algebra∎

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

The $C^{2}$ real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair

Statement

Let $f = u + i v$ be holomorphic on an open set $U \subseteq C$ , and assume $u, v \in C^{2} (U)$ . Then

$u_{x x} + u_{y y} = 0, v_{x x} + v_{y y} = 0.$

A $C^{2}$ real function satisfying this equation is called harmonic. Thus $u$ and $v$ are harmonic, and $v$ is a harmonic conjugate of $u$ in the sense that $u + i v$ is holomorphic. No automatic $C^{2}$ regularity or global existence of harmonic conjugates is asserted.

Facts & Assumptions

Given: A holomorphic $f = u + i v$ on $U$ with $u, v \in C^{2} (U)$ .

[L1]

Holomorphy gives $u_{x} = v_{y}$ and $u_{y} = - v_{x}$ (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).

[F1]

A $C^{2}$ function has continuous iterated partial derivatives through order two ( $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[L2]

If a function is $C^{2}$ on an open subset of $R^{m}$ , then its mixed second partial derivatives agree (Clairaut--Schwarz theorem for continuous second partial derivatives).

Proof

technique · direct

1.1

Differentiating $u_{x} = v_{y}$ in $x$ and $u_{y} = - v_{x}$ in $y$ gives $u_{x x} = v_{y x}$ and $u_{y y} = - v_{x y}$ .

givenL1F1

1.2

Differentiating $u_{x} = v_{y}$ in $y$ and $u_{y} = - v_{x}$ in $x$ gives $u_{x y} = v_{y y}$ and $u_{y x} = - v_{x x}$ .

givenL1F1

2.1

By [L2], $v_{y x} = v_{x y}$ , so step 1.1 gives $u_{x x} + u_{y y} = 0$ .

step 1.1L2algebra

3.1

By [L2], $u_{x y} = u_{y x}$ , so step 1.2 gives $v_{x x} + v_{y y} = 0$ . The terminology in the Statement now applies to the given pair $u, v$ .

step 1.2L2algebra∎

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

If a holomorphic function has $C^{2}$ components, then its derivative is holomorphic

Statement

Let $f = u + i v$ be holomorphic on an open set $U \subseteq C$ , and suppose $u, v \in C^{2} (U)$ . Then the complex derivative $f^{'} : U \to C$ is holomorphic.

Facts & Assumptions

Given: A holomorphic $f = u + i v$ with $C^{2}$ components.

[L1]

Holomorphy gives $f^{'} = u_{x} + i v_{x}$ and the equations $u_{x} = v_{y}$ , $u_{y} = - v_{x}$ (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).

[F1]

A $C^{2}$ function has continuous first and second partial derivatives ( $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[L2]

For $C^{2}$ functions, mixed second partial derivatives agree (Clairaut--Schwarz theorem for continuous second partial derivatives).

[L3]

Continuous first partial derivatives satisfying the Cauchy–Riemann equations imply holomorphy (Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set).

Proof

technique · direct

1.1

Write $f^{'} = p + i q$ with $p = u_{x}$ and $q = v_{x}$ . By [F1], the first partial derivatives of $p$ and $q$ exist and are continuous.

givenL1F1

1.2

Differentiating $u_{x} = v_{y}$ in $x$ and using [L2] gives $p_{x} = u_{x x} = v_{y x} = v_{x y} = q_{y}$ .

L1L2F1algebra

1.3

Differentiating $u_{y} = - v_{x}$ in $x$ and using [L2] gives $p_{y} = u_{x y} = u_{y x} = - v_{x x} = - q_{x}$ .

L1L2F1algebra

2.1

Thus $p, q$ have continuous first partials and satisfy the Cauchy–Riemann equations throughout $U$ , so [L3] makes $f^{'} = p + i q$ holomorphic.

step 1.1step 1.2step 1.3L3∎

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

The Hessian determinant of each $C^{2}$ holomorphic component is nonpositive; a nondegenerate critical point is a saddle

Statement

Let $f = u + i v$ be holomorphic with $C^{2}$ components. For either component $w \in {u, v}$ ,

$\det H_{w} = - w_{x x}^{2} - w_{x y}^{2} \leq 0.$

If $a$ is a critical point of $w$ and $\det H_{w} (a) \neq 0$ , then the determinant is negative and $a$ is neither a local maximum nor a local minimum, hence is a saddle in the Hessian-test sense. If the determinant is zero, the Hessian test is inconclusive.

Facts & Assumptions

Given: A holomorphic $f = u + i v$ whose components are $C^{2}$ , and one component $w$ .

[L1]

Each such component is harmonic: $w_{x x} + w_{y y} = 0$ (The $C^{2}$ real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair).

[F1]

The Hessian is the matrix of second partial derivatives, and a critical point is one at which the gradient vanishes (The Hessian matrix and critical points of a scalar field).

[L2]

For a $C^{2}$ function, $w_{x y} = w_{y x}$ (Clairaut--Schwarz theorem for continuous second partial derivatives).

[L3]

At a critical point of a $C^{2}$ function of two variables, a negative Hessian determinant gives neither a local minimum nor a local maximum, while determinant zero gives no conclusion (The two-variable Hessian determinant test).

Proof

technique · direct

1.1

By [F1] and [L2], $\det H_{w} = w_{x x} w_{y y} - w_{x y}^{2}$ . By [L1], $w_{y y} = - w_{x x}$ , so $\det H_{w} = - w_{x x}^{2} - w_{x y}^{2} \leq 0$ .

F1L1L2algebra

2.1

If the determinant at a critical point is nonzero, step 1.1 makes it negative, and [L3] gives neither a local maximum nor a local minimum. If it is zero, [L3] gives no conclusion.

step 1.1givenL3∎

5 · Examples, counterexamples and false statements

None yet.

Sources

Standard references

Recommended treatments; not extraction sources.

Complex Differentiability and the Cauchy–Riemann Equations

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

C=R[x]/(x2+1)C=R[x]/(x2+1) as the Euclidean plane and as a normed real algebra: what the identification preserves

A complex domain is a nonempty connected open subset of CC

Definition

Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions

Definition

The complex derivative at a point is unique

Statement

Facts & Assumptions

Proof

The Wirtinger derivatives ∂zf∂z​f and ∂zˉf∂zˉ​f, and antiholomorphic functions

Definition

Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with ∂zˉf=0∂zˉ​f=0, or with the Cauchy–Riemann equations

Statement

Facts & Assumptions

Proof

Complex differentiability at a point implies continuity there

Statement

Facts & Assumptions

Proof

Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set

Statement

Facts & Assumptions

Proof

Cartesian and polar forms of the Cauchy–Riemann equations agree away from the origin

Statement

Facts & Assumptions

Proof

Linearity, product, reciprocal, and quotient rules for complex derivatives

Statement

Facts & Assumptions

Proof

The chain rule for complex derivatives

Statement

Facts & Assumptions

Proof

The Wirtinger chain rule for compositions of real-differentiable complex-valued maps

Statement

Facts & Assumptions

Proof

A conjugate difference quotient characterizes antiholomorphic maps

Statement

Facts & Assumptions

Proof

A holomorphic function with continuous complex derivative has C1C1 real and imaginary components

Statement

Facts & Assumptions

Proof

A continuous local inverse has derivative reciprocal to a nonzero complex derivative

Statement

Facts & Assumptions

Proof

Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero

Statement

Facts & Assumptions

Proof

The complex exponential is entire and its complex derivative is itself

Statement

Facts & Assumptions

Proof

A holomorphic function with zero derivative on a domain is constant

Statement

Facts & Assumptions

Proof

A real-valued holomorphic function on a domain is constant

Statement

Facts & Assumptions

Proof

A holomorphic function of constant modulus on a domain is constant

Statement

Facts & Assumptions

Proof

If both ff and fˉfˉ​ are holomorphic on a domain, then ff is constant

Statement

Facts & Assumptions

Proof

$C = R [x] / (x^{2} + 1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves

A complex domain is a nonempty connected open subset of $C$

The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions

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

A holomorphic function with continuous complex derivative has $C^{1}$ real and imaginary components

If both $f$ and $\overset{ˉ}{f}$ are holomorphic on a domain, then $f$ is constant

The Jacobian determinant of a holomorphic map is $∣ f^{'} ∣^{2}$ and is positive exactly where $f^{'} \neq 0$

The $C^{2}$ real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair

If a holomorphic function has $C^{2}$ components, then its derivative is holomorphic

The Hessian determinant of each $C^{2}$ holomorphic component is nonpositive; a nondegenerate critical point is a saddle