TheoremStatement: Literature-sourcedProof: AI-adapted

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]

Apply The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ to $f_{R}$ and $g_{R}$ on their open coordinate domains. By Real total derivatives transport through the complex coordinate isometry, conjugating the resulting identity by $Φ^{- 1}$ and $Φ$ gives $D_{R} (g \circ f) (a) = D_{R} g (f (a)) \circ D_{R} 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.1givenF1

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}$ .

1.2F1L2algebra

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.

2.1step 1.1L1L2algebra

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

3.1step 2.1F1algebra∎

A real-linear map has unique coefficients $P, Q$ in $P h + Q \overset{ˉ}{h}$ : its values at $1$ and $i$ give $P + Q$ and $i (P - Q)$ , which determine $P, Q$ . Comparing step 2.1 with this unique 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}$ .

Depends on

Used by

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Lebl, Guide to Cultivating Complex Analysis, Exercise 2.2.10 (standard reference, not scraped)