TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

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∎

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: 44 results over 11 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. Lebl, Guide to Cultivating Complex Analysis, Exercise 2.2.10 (standard reference, not scraped)