LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Calculus of holomorphic maps: chain rule, Wirtinger derivatives, coefficient extraction in one variable, and locally uniform limits

Statement

Let $m, l, p \geq 1$ and let $D \subseteq C^{m}$ , $D^{'} \subseteq C^{l}$ be open, with holomorphy in the sense of Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket.

Chain rule. If $g : D^{'} \to D$ and $F : D \to C^{p}$ are holomorphic, then $F \circ g : D^{'} \to C^{p}$ is holomorphic and $D (F \circ g) (z) = D F (g (z)) \circ D g (z) (z \in D^{'}) .$
Wirtinger derivatives and the bracket matrix. If $f : D \to C$ is holomorphic, then $f$ is totally differentiable as a map of $R^{2 m}$ and, writing $x_{k}, y_{k}$ for the real and imaginary parts of $z_{k}$ , $\partial_{{\overset{ˉ}{z}}_{k}} f : = \frac{1}{2} (\partial_{x_{k}} f + i \partial_{y_{k}} f) = 0, \partial_{z_{k}} f : = \frac{1}{2} (\partial_{x_{k}} f - i \partial_{y_{k}} f) = D f (e_{k}) .$ Consequently, for holomorphic $f, g$ on a complex phase domain $D \subseteq C^{2 d}$ , with $\nabla f = (\partial_{z^{1}} f, \dots, \partial_{w_{d}} f)$ and $J$ the standard matrix, ${f, g} = (\nabla f)^{T} J \nabla g .$
Coefficient extraction in a complex step variable. Let $0 < σ \leq \infty$ and let $D \subseteq C^{m}$ be open, and let $F : {∣ h ∣ < σ} \times D \to C^{p}$ be holomorphic. Then for every $j \in N$ the coefficient map $c_{j} (z) : = \partial_{h}^{j} F (0, z) / j!$ is holomorphic on $D$ , and for every $0 < s < σ$ , $c_{j} (z) = \frac{1}{2 π i} \oint_{∣ h ∣ = s} \frac{F (h, z)}{h^{j + 1}} d h$ .
Locally uniform limits. For maps $F_{n}, F : D \to C^{p}$ , define locally uniform convergence here to mean that for every nonempty compact $C \subseteq D$ and every $ε > 0$ there is $n_{0}$ such that $\sup_{z \in C} ∥ F_{n} (z) - F (z) ∥ < ε$ for all $n \geq n_{0}$ , with the Euclidean norm on $C^{p}$ . This is equivalent to uniform convergence of each of the finitely many scalar components on every such $C$ , since $∣ v_{i} ∣ \leq ∥ v ∥ \leq \sqrt{p} \max_{i} ∣ v_{i} ∣$ . On one-variable scalar slices it agrees with Locally uniform convergence on an open subset of the complex plane is compact convergence and Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary. If all $F_{n}$ are holomorphic and converge in this sense to $F$ , then $F$ is holomorphic on $D$ .

Facts & Assumptions

Given: The open sets $D, D^{'}$ and the holomorphic maps named in each clause; $C^{m} ≅ R^{2 m}$ throughout ( $C = R [x] / (x^{2} + 1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves, $C$ is the real coordinate plane, with coordinate arithmetic).

[L1]

$C$ -linear maps are $R$ -linear, and the real total derivative of a holomorphic map equals its $C$ -linear derivative read on $R^{2 m}$ ; moreover a composition of $C$ -linear maps is $C$ -linear (Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket, The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[L2]

The chain rule for total derivatives: $D (G \circ H) (x) = D G (H (x)) \circ D H (x)$ ; and the partial derivatives in the coordinate directions are the entries of the total derivative (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, $C^{k}$ Euclidean maps and diffeomorphisms).

[L3]

Cauchy formula in one variable and Taylor coefficients: for holomorphic $G$ on $D (h_{0}, s)$ and $0 < s^{'} < s$ , $\partial^{j} G (h_{0}) / j! = \frac{1}{2 π i} \oint_{∣ h - h_{0} ∣ = s^{'}} G (h) (h - h_{0})^{- j - 1} d h$ (Iterated Cauchy formula, power-series expansion and Cauchy estimates for functions continuous and separately holomorphic on a polydisc, clause 2, with $m = 1$ ; Cauchy's inequalities bound the Taylor coefficients by the circle supremum).

[L4]

Parameter integrals: a jointly continuous $φ : [0, 2 π] \times Ω \to C$ with $h$ -slice holomorphic in the parameter $z \in Ω$ has holomorphic parameter integral (A jointly continuous finite-interval parameter integral of holomorphic functions is holomorphic); and a locally uniform limit of holomorphic one-variable functions is holomorphic (Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).

[L5]

Continuity: uniform limits of continuous complex-valued maps are continuous (A uniform limit of continuous complex-valued functions is continuous); a holomorphic function of several variables is continuous, because differentiability at every point implies continuity (Complex phase domains, holomorphic maps on $C^{m}$ , and the complexified canonical form and bracket).

[L6]

The matrix identity: for $\nabla f, \nabla g$ as in clause 2, $(\nabla f)^{T} J \nabla g = \sum_{i} (\partial_{z^{i}} f \partial_{w_{i}} g - \partial_{w_{i}} f \partial_{z^{i}} g)$ , by block multiplication (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The transpose $A^{T}$ of a matrix).

Proof

technique · direct; compose derivatives, decompose the complex derivative into real partials, and use one-variable Cauchy theory slice by slice

1.1givenL1L2

Clause 1. A holomorphic map is totally differentiable as a real map with $D_{R} F = D F$ by [L1], so [L2] applies to $F \circ g$ : it is totally differentiable with derivative $D F (g (z)) \circ D g (z)$ , a composite of $C$ -linear maps, hence $C$ -linear by [L1]. Since $z$ was arbitrary, $F \circ g$ is holomorphic with the displayed derivative.

1.2givenL1L2L6

Clause 2. Let $f$ be holomorphic and fix $k$ . The partial derivatives $\partial_{x_{k}} f, \partial_{y_{k}} f$ exist and are the images under $D f$ of the real basis vectors $e_{x_{k}}, e_{y_{k}}$ by [L2]; because $D f$ is $C$ -linear, $D f (e_{y_{k}}) = D f (i e_{x_{k}}) = i D f (e_{x_{k}})$ , that is, $\partial_{y_{k}} f = i \partial_{x_{k}} f$ . Hence $\partial_{{\overset{ˉ}{z}}_{k}} f = \frac{1}{2} (\partial_{x_{k}} f + i i \partial_{x_{k}} f) = 0$ and $\partial_{z_{k}} f = \frac{1}{2} (\partial_{x_{k}} f - i i \partial_{x_{k}} f) = \partial_{x_{k}} f = D f (e_{k})$ . The matrix identity of clause 2 is then exactly [L6].

1.3givenL3L4L5

Clause 3, holomorphy of $c_{j}$ . For fixed $z \in D$ the map $h \mapsto F (h, z)$ is holomorphic on ${∣ h ∣ < σ}$ (composition of the holomorphic $F$ with the holomorphic slice injection, clause 1), so $c_{j} (z)$ is well defined and equals the contour integral of [L3]. To see that $z \mapsto c_{j} (z)$ is holomorphic, fix one coordinate $z_{k}$ and hold the others; the integrand $φ (h, z_{k}) : = F (h, z) h^{- j - 1}$ is, on the compact circle ${∣ h ∣ = s}$ times a small disc in $z_{k}$ , jointly continuous because $F$ is continuous by [L5], and holomorphic in $z_{k}$ for each $h$ because the slice $z \mapsto F (h, z)$ is holomorphic (clause 1). By [L4] applied to the parametrized integral, $c_{j}$ is holomorphic in $z_{k}$ on that disc; hence each scalar component of $c_{j}$ is separately holomorphic, and it is continuous as an integral of a jointly continuous family on a compact contour. By Iterated Cauchy formula, power-series expansion and Cauchy estimates for functions continuous and separately holomorphic on a polydisc applied componentwise to $c_{j}$ on a polydisc around any point, $c_{j}$ is holomorphic on $D$ : assemble the finitely many complex-linear component derivatives, whose remainder norm is at most $\sqrt{p}$ times the largest scalar remainder.

2.1givenstep 1.3L4L5

Clause 4. Around any $a \in D$ choose a closed polydisc contained in $D$ . It is compact, so convergence is uniform there in the Euclidean target norm. Continuity of $F$ at $a$ follows from $∥ F (z) - F (a) ∥ \leq ∥ F (z) - F_{n} (z) ∥ + ∥ F_{n} (z) - F_{n} (a) ∥ + ∥ F_{n} (a) - F (a) ∥$ , first choosing $n$ to make both uniform errors less than $ε / 3$ , then choosing $z$ close enough to $a$ for the middle term. Apply the remaining argument to each scalar component: fixing all coordinates but one, the slice $F_{n} (\dots, \cdot, \dots)$ is a locally uniform limit of holomorphic one-variable functions, hence holomorphic by [L4]; thus each scalar component is continuous and separately holomorphic on $D$ , and Iterated Cauchy formula, power-series expansion and Cauchy estimates for functions continuous and separately holomorphic on a polydisc makes it holomorphic. Assemble their derivatives as in step 1.3 to obtain a complex-linear derivative of $F$ , with vector remainder $o (∥ v ∥)$ .

3.1step 1.1step 1.2step 1.3step 2.1∎

Conclusion. Clause 1 is step 1.1, clause 2 is step 1.2, clause 3 is step 1.3 and clause 4 is step 2.1.

Remarks

Clause 3 is applied on this page to families $h \mapsto L_{h} f$ whose coefficients are the field components $X_{j}$ ; it is the only place where the analytic (rather than merely formal) dependence on the complex step variable is used.
Clause 1 for $l = 1$ and $D^{'}$ a disc is used to see that $h \mapsto Ψ_{h} (z)$ is holomorphic in $h$ for fixed $z$ , once the joint holomorphy of $(h, z) \mapsto Ψ_{h} (z)$ is available from The flow of a bounded holomorphic field on a polydisc: existence in complex time, displacement bound, holomorphy, and the composition law.

Depends on

Dependency tree · 2 levels

Sources

J. Lebl, Tasty Bits of Several Complex Variables, Chapter 1, Sections 1.1-1.3 (holomorphic maps, power series, derivatives), printed pages 13-31