Several complex variables

This umbrella imports the classical function theory of open subsets of finite-dimensional complex normed spaces. Analytic maps use Mathlib's AnalyticOnNhd ℂ; holomorphic maps on open sets use DifferentiableOn ℂ. Banach-valued targets are retained where appropriate. Finite coordinate spaces carry the supremum norm, so their balls are polydiscs; Euclidean ball geometry uses the inner-product norm explicitly.

Local analysis and function spaces

The library provides polydisc Cauchy and Taylor formulas with separate radii, mixed derivative estimates, the Cauchy–Riemann equations, the identity and maximum principles, analytic parameter integrals, and the Cauchy–Pompeiu identity. Locally uniform convergence preserves analyticity and derivatives. Holomorphic maps form compact-open function spaces, with continuous evaluation, restriction, and coordinate differentiation. Montel and Vitali theorems use finite-dimensional targets for compactness. Holomorphic Lp spaces are complete, including exponent infinity.

Mapping theory and continuation

Inverse and implicit mapping theorems, regular zero-set graphs, injective holomorphic maps, Cartan uniqueness, circular rigidity, and explicit ball automorphisms are included. Reinhardt, circular, and Hartogs geometry support Taylor and Laurent continuation, unrestricted separate holomorphy, and removable singularities. Hartogs' compact-hole theorem follows from Ehrenpreis' argument with real derivatives and the Cauchy transform, without differential forms.

Germs and analytic sets

Analytic germs form local integral domains with residue field ℂ. Weierstrass division and preparation, Taylor uniqueness, coordinate-independent total order, Noetherianity, and unique factorization support zero-set and relative-primality results. Analytic subsets have local finite equations, interior rigidity, dense connected complements, and regular and singular loci. The Riemann extension theorems include Banach-valued removal and the holomorphic restriction algebra equivalence across sets of slice codimension at least two.

Convexity, boundary geometry, and approximation

Holomorphic hulls, compact exhaustions, and escaping sequences lead to the Cartan–Thullen equivalences on finite-dimensional complex normed spaces. Thullen's Banach-valued Taylor continuation lemma gives the coordinate hull-radius statements and Bochner's tube theorem. Subharmonicity and plurisubharmonicity use the local submean property; the Laplacian and Levi form give their C² criteria. Domains of holomorphy are pseudoconvex and satisfy continuity principles. Levi's necessary condition, independence of the defining function, holomorphic supporting polynomials, normalized local peak functions, and local holomorphic blow-up are proved. Runge pairs and domains use approximation on compact sets; polynomial hulls and Reinhardt and circular examples are included.

The Oka–Weil theorem, the Levi sufficiency problem, and abstract envelopes of holomorphy remain outside this library's scope. The upstream theorem catalogue records the precise mathematical statements at the imported revision.