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.
Complex -space and its real coordinate dictionary
Remark
Fix a natural number . Complex -space is the set of functions , so a point has coordinates for , indexed from exactly as is in this library. With coordinatewise addition and multiplication by complex scalars it is a vector space over the field (Vector space over a field, is a field, every element is uniquely , and every nonzero element has inverse ), with the standard basis of The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension .
The coordinate identification. Writing with real (Real and imaginary parts, complex conjugation, and modulus), define
The interleaved ordering is the one used throughout this page; the ordering that groups all real parts before all imaginary parts is a different bijection, and nothing below is stated for it. is a bijection and is -linear.
Norms agree. Put . Since , this is the Euclidean norm of The -norms for rational , and and The Euclidean inner product on , and it is a norm on the real vector space underlying in the sense of A norm on a real vector space, the induced metric, and the dictionary with the metric axioms. Consequently , so the metric of , its balls (Open ball, closed ball and sphere in a metric space), its open sets, its convergent sequences, its Cauchy sequences and its continuous maps are verbatim those of under . In particular convergence and continuity are coordinatewise (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, Vector-valued functions , their limits and continuity, with the dictionary to the metric notions), is complete (For a sequence in converges iff each coordinate sequence converges, is Cauchy iff each coordinate sequence is Cauchy, and is complete in every norm), and a subset of is compact exactly when it is closed and bounded (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
At this is the published plane dictionary. For the map is the bijection of as the Euclidean plane and as a normed real algebra: what the identification preserves and every clause above reduces to a clause recorded there. Openness, connectedness and real total differentiability on are always read through , exactly as that remark reads them through its own identification.
What does not carry. respects the additive and the real scalar structure but not multiplication by in any way visible to a general -linear map of : an -linear map of need not be -linear. That distinction is the whole content of the criterion the page proves next, and it is why "linear" is always qualified below.
Depends on
- $\mathbb C=\mathbb R[x]/(x^2+1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- The $p$-norms $\lVert x\rVert_p$ for rational $p \ge 1$, and $\lVert x\rVert_\infty$
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- For $n \ge 1$ a sequence in $\mathbb{R}^n$ converges iff each coordinate sequence converges, is Cauchy iff each coordinate sequence is Cauchy, and $\mathbb{R}^n$ is complete in every norm
- A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions
- Vector-valued functions $f : A \to \mathbb{R}^m$, their limits and continuity, with the dictionary to the metric notions
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- 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$
- Real and imaginary parts, complex conjugation, and modulus
- Vector space over a field
- $\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)$
- Open ball, closed ball and sphere in a metric space
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
- The modulus of a holomorphic function on a closed polydisc is bounded by its supremum on the distinguished boundary Corollary
- A nonzero holomorphic function on ℂ² whose zero set is an unbounded hyperplane Counterexample
- Balls, polydiscs and the distinguished boundary in ℂᵐ Definition
- Holomorphic functions on an open subset of ℂᵐ Definition
- Holomorphic maps ℂᵐ → ℂⁿ and the complex Jacobian matrix Definition
- Multi-indexed power series in ℂᵐ and their absolute convergence Definition
- Separately holomorphic functions Definition
- Wirtinger operators in ℂᵐ Definition
- A bounded separately holomorphic function on a polydisc is Lipschitz on every smaller polydisc Lemma
- A real-linear functional on ℂᵐ is complex linear exactly when its antiholomorphic part vanishes Lemma
- The Cauchy kernel expands as an absolutely and uniformly convergent multi-indexed geometric series 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 continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc Theorem
- 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
- Cauchy estimates for mixed derivatives on a polydisc 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
- Locally uniform limits of holomorphic functions are holomorphic, with locally uniform convergence of all derivatives Theorem
- Osgood's lemma: continuous and separately holomorphic implies holomorphic Theorem
- The composite of holomorphic maps is holomorphic and its complex Jacobian is the product Theorem
- The iterated Cauchy integral formula on a polydisc Theorem
Dependency tree · two levels
110 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.1 (standard reference, not scraped)