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.
Wirtinger operators in
Definition
Fix , let be open and let . Read as through Complex -space and its real coordinate dictionary, with real coordinates for given by (Real and imaginary parts, complex conjugation, and modulus), and let and be the partial derivatives of Directional derivatives and partial derivatives of a map applied to the two real components of and recombined.
At a point where all of these partial derivatives exist, define the Wirtinger operators
The differential identity. Suppose in addition that is real totally differentiable at a point , so that is the -linear map with for , by A total derivative computes every directional derivative, and its matrix is the Jacobian read in the standard basis (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ). Substituting and and collecting the coefficients of and using finite sums in the additive commutative monoid of (A finite sum in a commutative monoid indexed by an arbitrary finite set) and distributivity in the complex field ( is a field, every element is uniquely , and every nonzero element has inverse ) gives
Indeed the coefficient of is , and the coefficient of is .
Remarks
At these are the published Wirtinger derivatives. The two displayed formulas are literally those of The Wirtinger derivatives and , and antiholomorphic functions with written , and the differential identity reduces to the identity recorded there.
These are operators on real-differentiable functions, not on holomorphic ones. Nothing above assumes any complex differentiability: the definition needs only the real partial derivatives, and the differential identity needs only real total differentiability. Which functions have all is the question the next lemma and the Cauchy–Riemann characterisation answer.
Depends on
- Complex $m$-space and its real coordinate dictionary
- The Wirtinger derivatives $\partial_z f$ and $\partial_{\bar z}f$, and antiholomorphic functions
- Directional derivatives and partial derivatives of a map $U\subseteq\mathbb{R}^m\to\mathbb{R}^n$
- The total (Fréchet) derivative $Df(a)$ as the linear first-order approximation with $o(\|h\|_2)$ remainder
- 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
- Real and imaginary parts, complex conjugation, and modulus
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- A finite sum in a commutative monoid indexed by an arbitrary finite set
- $\mathbb C=\mathbb R[x]/(x^2+1)$ is a field, every element is uniquely $a+bi$, and every nonzero element has inverse $(a-bi)/(a^2+b^2)$
Used by
- Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic Corollary
- Holomorphic maps ℂᵐ → ℂⁿ and the complex Jacobian matrix Definition
- A real-linear functional on ℂᵐ is complex linear exactly when its antiholomorphic part vanishes Lemma
- A holomorphic function of several variables is continuous and separately holomorphic Proposition
- Sums, products and nonvanishing quotients of holomorphic functions are holomorphic Proposition
- A map into ℂⁿ is holomorphic exactly when each of its components is Theorem
- An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise Theorem
- For C¹ functions, holomorphy, complex linearity of the real derivative, and the Cauchy–Riemann system agree Theorem
Dependency tree · two levels
52 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, Tasty Bits of Several Complex Variables, §1.3 (standard reference, not scraped)