TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13

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.

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∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 71 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Orloff, MIT 18.04 Topic 2, Theorem 2.13 (standard reference, not scraped)

If a holomorphic function has C2C2 components, then its derivative is holomorphic