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.
Holomorphic functions on an open subset of
Definition
Fix , read through Complex -space and its real coordinate dictionary, and let be open and .
A map is -linear when and for all and all , the vector-space operations being those of Vector space over a field over the field ( is a field, every element is uniquely , and every nonzero element has inverse ). Requiring the second clause only for real gives the strictly weaker notion of an -linear map (A linear map in Euclidean coordinates) read through the dictionary.
A function is complex differentiable at when there is a -linear with
the quotient being considered for with and the norm being that of the dictionary (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms). The map is holomorphic on when it is complex differentiable at every point of .
Such an is unique, so the notation is well posed. If and both satisfy the condition, then is -linear and ; fixing and taking replaced by for real small enough that , -linearity gives , whose limit as is ; so for every .
Remarks
No continuity and no local boundedness are built in. The definition asks for the linear approximation and nothing else. That a holomorphic function is continuous is proved on this page rather than assumed, and the two theorems that recover holomorphy from separate holomorphy — under continuity, and under local boundedness — are theorems precisely because those properties are not part of the definition. Defining holomorphy by local power-series representability or by the Cauchy–Riemann system, as some treatments do, would make one or other of them a tautology.
At this is the published one-variable notion. A -linear satisfies , so with the condition reads with , which is exactly complex differentiability at with in the sense of Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions; conversely that condition produces the -linear map .
Relation to the real total derivative. Reading as a map through the dictionary, the displayed condition is the total-differentiability condition of The total (Fréchet) derivative as the linear first-order approximation with remainder with the extra requirement that the approximating linear map be -linear and not merely -linear. So a complex differentiable is real totally differentiable with as its real total derivative, and The total derivative at a point is unique says the two uses of the notation cannot disagree. The standard basis vectors of The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension are the ones used to read off coordinates of .
Depends on
- Complex $m$-space and its real coordinate dictionary
- Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions
- Vector space over a field
- A linear map $L:\mathbb{R}^m\to\mathbb{R}^n$ in Euclidean coordinates
- The total derivative at a point is unique
- The total (Fréchet) derivative $Df(a)$ as the linear first-order approximation with $o(\|h\|_2)$ remainder
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- $\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)$
- 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$
Used by
- A bounded holomorphic function on all of ℂᵐ is constant Corollary
- Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic Corollary
- A nonzero holomorphic function on ℂ² whose zero set is an unbounded hyperplane Counterexample
- Holomorphic maps ℂᵐ → ℂⁿ and the complex Jacobian matrix Definition
- The complex Jacobian and its determinant for (z₀z₁, z₀+z₁) Example
- A holomorphic function on a domain in ℂ² vanishing on a set with an accumulation point vanishes identically False statement
- 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
- Conventions on this page, and what the several-variable identity theorem does not say Remark
- A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically Theorem
- A map into ℂⁿ is holomorphic exactly when each of its components is Theorem
- A nonconstant scalar holomorphic function on a domain in ℂᵐ is an open map Theorem
- An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise Theorem
- An interior local maximum of the modulus forces a scalar holomorphic function to be constant Theorem
- For C¹ functions, holomorphy, complex linearity of the real derivative, and the Cauchy–Riemann system agree Theorem
- Locally bounded and separately holomorphic implies holomorphic Theorem
- Osgood's lemma: continuous and separately holomorphic implies holomorphic Theorem
Dependency tree · two levels
57 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.2 (standard reference, not scraped)