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
- Hartogs extension by a compact-support dbar correction Corollary
- Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic Corollary
- Positive-degree Dolbeault vanishing on pseudoconvex domains 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
- Meromorphic functions on an open set in complex Euclidean space Definition
- Multi-indexed power series in ℂᵐ and their absolute convergence Definition
- Separately holomorphic functions Definition
- The Bergman space A²(Ω) and the Bergman kernel Definition
- The Jacobian of a compact Riemann surface Definition
- The Levi form and strict plurisubharmonicity Definition
- Weighted L2 spaces and maximal dbar operators Definition
- Wirtinger operators in ℂᵐ Definition
- A Hartogs domain with a strictly plurisubharmonic exhaustion Example
- A strictly plurisubharmonic exhaustion of the convex unit ball Example
- An explicit ∂̄ solution with an L² estimate Example
- Ball monomial norms, Bergman and Szegő kernels of the ball Example
- Cutoff extension across a puncture in complex dimension two Example
- Hörmander estimate with a Gaussian weight Example
- Levi form of the unit ball Example
- The polydisc boundary is not a smooth hypersurface, so the Szegő definition does not apply Example
- The unit ball is Levi pseudoconvex Example
- The claim that the ball and the polydisc are biholomorphic False statement
- 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
- Determinants and kernel quotients of the model Bergman metrics Lemma
- Locally finite smooth partitions of unity on domains Lemma
- Monomial integrals on the sphere and orthonormality on the distinguished torus Lemma
- Monomials form complete orthogonal systems of the Bergman spaces of the disc, the ball and the polydisc Lemma
- Polynomial traces, monomial basis and bounded evaluation for the ball Hardy space Lemma
- Smoothness of the Bergman kernel and positivity of its diagonal on bounded domains Lemma
- Sup-norm and first-derivative bounds by the L² norm on compact subsets Lemma
- The Cauchy kernel expands as an absolutely and uniformly convergent multi-indexed geometric series Lemma
- The complex Hessian of a C² function dominates that of a minorant at a common minimum Lemma
- The mean-value L² bound for holomorphic functions on a polydisc Lemma
- Weighted monomial integrals and monomial norms for the disc, ball and polydisc Lemma
…and 22 more results.
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)