Several complex variables: principal statements (Solution.lean)

This file states the principal results of the SeveralComplexVariables library in terms of Mathlib alone. Its numbering follows the upstream theorem catalogue at the imported revision: the number in each docstring is the item of that catalogue, and A–K are its sections. The subject is classical function theory on open subsets of finite-dimensional complex normed spaces E, in particular of ℂ^ι = ι → ℂ for a finite index type ι, with values in a complex Banach space F.

Conventions

• Holomorphic is DifferentiableOn ℂ f U and analytic is AnalyticOnNhd ℂ f U. On open subsets of E the two agree (item 3), and the statements use whichever the library proves directly.
• ι → ℂ carries the supremum norm, so that Metric.ball is a polydisc with equal radii; a polydisc with separate radii is Set.pi univ fun i => Metric.ball (c i) (r i). Dimension zero and empty index types are included unless a hypothesis excludes them.
• Domains are not assumed connected or nonempty; such hypotheses are stated where they are needed.
• Hulls are defined through all real upper bounds rather than suprema. Subharmonic and plurisubharmonic functions are real valued, so the value -∞ is not admitted.
• The definitions below restate those of the library and are kept few. Where a notion is used once, it is written out in the statement instead.

Scope

Of the 65 items of the catalogue, all are represented except items 42 and 43 (factors of distinguished polynomials, and the comparison of polynomials over the germ ring with germs), which are algebraic steps towards items 44 and 45. An item with several assertions is represented by its principal assertion. The sources are the texts of Boas, Fritzsche–Grauert, Hörmander, Jakóbczak–Jarnicki, Korevaar–Wiegerinck, Range, Scheidemann, Shabat and Suwa listed in the upstream bibliography; none of the results is new. The proofs use only the axioms propext, Quot.sound and Classical.choice.

Related formalizations

The development builds on Mathlib. Lean Pool already contains Bochao Kong's analytic Weierstrass preparation theorem with germ uniqueness as ClassicalComplexWPT.classicalComplexWeierstrassPreparation, and coordinate-origin germ Noetherianity as LocalComplexGeometry.holomorphicGerm_isNoetherian. These overlap items 41 and 44 here. At coordinate origins, both developments model analytic germs as the subring of Mathlib's Filter.Germ consisting of germs with an analytic representative.

This import retains its independent analytic division and preparation arguments, including quotient estimates, and transports the local statements to arbitrary finite-dimensional complex normed spaces and base points. Its further results include germ unique factorization and relative primality, Hartogs extension, Cartan–Thullen equivalences, and Bochner's tube theorem. These additional results supply the project's broader scope. The local analytic Nullstellensatz in LeanPool.LocalComplexGeometry is not treated here.

A. Local analysis and differential calculus

noncomputable def SCV.partialDeriv {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {ι : Type u_3} [DecidableEq ι] (i : ι) (f : (ι → ℂ) → F) (z : ι → ℂ) : F

The derivative in the coordinate i, the other coordinates being fixed.

Equations

• SCV.partialDeriv i f z = deriv (fun (w : ℂ) => f (Function.update z i w)) (z i)

noncomputable def SCV.iteratedPartialDeriv {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {ι : Type u_3} [DecidableEq ι] : List ι → ((ι → ℂ) → F) → (ι → ℂ) → F

The iterated coordinate derivative along a list of coordinates; the leftmost acts last.

Equations

• SCV.iteratedPartialDeriv [] x✝ = x✝
• SCV.iteratedPartialDeriv (i :: is) x✝ = SCV.partialDeriv i (SCV.iteratedPartialDeriv is x✝)

theorem SCV.cauchy_formula_polydisc {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {n : ℕ} {f : (Fin n → ℂ) → F} {c w : Fin n → ℂ} {R : Fin n → ℝ} (hR : ∀ (i : Fin n), 0 < R i) (hw : ∀ (i : Fin n), ‖w i - c i‖ < R i) (hfc : ContinuousOn f (Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (R i))) (hfa : ∀ z ∈ Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (R i), ∀ (i : Fin n), AnalyticAt ℂ (fun (x : ℂ) => f (Function.update z i x)) (z i)) : (((2 * ↑Real.pi * Complex.I) ^ n)⁻¹ • ∯ (z : Fin n → ℂ) in T(c, R), (∏ i : Fin n, (z i - w i)⁻¹) • f z) = f w

1. Cauchy's integral formula on a polydisc, for a function continuous on the closed polydisc and analytic in each variable separately.

theorem SCV.osgood {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hU : IsOpen U) (hfc : ContinuousOn f U) (hf : ∀ z ∈ U, ∀ (i : ι), AnalyticAt ℂ (fun (w : ℂ) => f (Function.update z i w)) (z i)) : AnalyticOnNhd ℂ f U

2. Osgood's lemma: a continuous, separately analytic function is jointly analytic.

theorem SCV.differentiableOn_iff_analyticOnNhd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set E} {f : E → F} (hU : IsOpen U) : DifferentiableOn ℂ f U ↔ AnalyticOnNhd ℂ f U

3. Holomorphic is analytic on open subsets of a finite-dimensional space, for Banach-valued maps.

theorem SCV.analyticOnNhd_iff_cauchyRiemann {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {U : Set (ι → ℂ)} (hU : IsOpen U) {f : (ι → ℂ) → F} : AnalyticOnNhd ℂ f U ↔ (∀ z ∈ U, DifferentiableAt ℝ f z) ∧ ∀ z ∈ U, ∀ (i : ι), (fderiv ℝ f z) (Pi.single i Complex.I) = Complex.I • (fderiv ℝ f z) (Pi.single i 1)

4. Cauchy–Riemann equations: holomorphy is real differentiability together with the coordinate Cauchy–Riemann equations.

theorem SCV.identity_theorem {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U V : Set E} (hU : IsOpen U) (hconn : IsPreconnected U) {f g : E → F} (hf : DifferentiableOn ℂ f U) (hg : DifferentiableOn ℂ g U) (hV : IsOpen V) (hne : V.Nonempty) (hVU : V ⊆ U) (heq : Set.EqOn f g V) : Set.EqOn f g U

6. Identity theorem: holomorphic maps on a connected open set that agree on a nonempty open subset agree everywhere.

theorem SCV.maximum_modulus {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] [StrictConvexSpace ℝ F] {U : Set E} (hU : IsOpen U) (hconn : IsPreconnected U) {f : E → F} (hf : DifferentiableOn ℂ f U) {a : E} (ha : a ∈ U) (hmax : IsLocalMax (norm ∘ f) a) : Set.EqOn f (Function.const E (f a)) U

7. Maximum modulus principle, for maps into a strictly convex Banach space, in particular for scalar functions.

theorem SCV.cauchy_pompeiu {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {φ : ℂ → F} (hφ : ContDiff ℝ 1 φ) (hsupp : HasCompactSupport φ) : ∫ (w : ℂ), w⁻¹ • 2⁻¹ • ((fderiv ℝ φ w) 1 + Complex.I • (fderiv ℝ φ w) Complex.I) = -(↑Real.pi • φ 0)

9. Cauchy–Pompeiu identity for a compactly supported C¹ function, with the antiholomorphic derivative (∂φ/∂x + i ∂φ/∂y) / 2 written via the real derivative.

noncomputable def SCV.taylorSeries {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {n : ℕ} (f : (Fin n → ℂ) → F) (c : Fin n → ℂ) : MvPowerSeries (Fin n) F

The Taylor series at c of a function of n complex variables: the coefficient of zᵐ is ∂ᵐ f (c) / m!, the mixed derivative being taken coordinate by coordinate.

Equations

• SCV.taylorSeries f c m = (∏ i : Fin n, ↑(m i).factorial)⁻¹ • SCV.iteratedPartialDeriv (List.ofFn fun (i : Fin n) => List.replicate (m i) i).flatten f c

theorem SCV.cauchy_estimates {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {n : ℕ} {U : Set (Fin n → ℂ)} (hU : IsOpen U) {f : (Fin n → ℂ) → F} (hf : DifferentiableOn ℂ f U) {c : Fin n → ℂ} {R : Fin n → ℝ} (hR : ∀ (i : Fin n), 0 < R i) {M : ℝ} (hsub : (Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (R i)) ⊆ U) (hM : ∀ z ∈ Set.univ.pi fun (i : Fin n) => Metric.closedBall (c i) (R i), ‖f z‖ ≤ M) (m : Fin n →₀ ℕ) : ‖taylorSeries f c m‖ ≤ M * ∏ i : Fin n, (R i)⁻¹ ^ m i

5. Cauchy estimates for the Taylor coefficients of a function holomorphic near a closed polydisc and bounded by M on it.

theorem SCV.analyticOnNhd_integral {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {α : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {U : Set E} {G : E → α → F} (hU : IsOpen U) (hmeas : ∀ x ∈ U, MeasureTheory.AEStronglyMeasurable (G x) μ) (hderivmeas : ∀ x ∈ U, MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℂ (fun (x : E) => G x a) x) μ) (hhol : ∀ᵐ (a : α) ∂μ, AnalyticOnNhd ℂ (fun (x : E) => G x a) U) (hdom : ∀ x ∈ U, ∃ (s : Set E) (bound : α → ℝ), s ∈ nhds x ∧ MeasureTheory.Integrable bound μ ∧ ∀ᵐ (a : α) ∂μ, ∀ y ∈ s, ‖G y a‖ ≤ bound a) : AnalyticOnNhd ℂ (fun (x : E) => ∫ (a : α), G x a ∂μ) U

8. Holomorphic dependence of integrals on parameters, under a locally integrable bound.

B. Convergence and spaces of holomorphic functions

theorem SCV.weierstrass_convergence {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set E} (hU : IsOpen U) {f : ℕ → E → F} {g : E → F} (hf : ∀ (n : ℕ), DifferentiableOn ℂ (f n) U) (hlim : TendstoLocallyUniformlyOn f g Filter.atTop U) : DifferentiableOn ℂ g U ∧ TendstoLocallyUniformlyOn (fun (n : ℕ) => fderiv ℂ (f n)) (fderiv ℂ g) Filter.atTop U

10. Weierstrass convergence theorem: a locally uniform limit of holomorphic maps is holomorphic, and the derivatives converge locally uniformly.

def SCV.holomorphicMaps {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : TopologicalSpace.Opens E) (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℂ F] : Set C(↥U, F)

The continuous maps on an open set U that are restrictions of holomorphic maps.

Equations

• SCV.holomorphicMaps U F = {f : C(↥U, F) | ∃ (g : E → F), DifferentiableOn ℂ g ↑U ∧ ∀ (z : ↥U), g ↑z = f z}

theorem SCV.isClosed_holomorphicMaps {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (U : TopologicalSpace.Opens E) : IsClosed (holomorphicMaps U F)

11. Holomorphic function spaces: the holomorphic maps form a closed subset of C(U, F) in the compact-open topology.

theorem SCV.montel {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] [FiniteDimensional ℂ F] {U : Set E} (hU : IsOpen U) {f : ℕ → E → F} (hf : ∀ (n : ℕ), DifferentiableOn ℂ (f n) U) {M : ℝ} (hM : ∀ (n : ℕ), ∀ z ∈ U, ‖f n z‖ ≤ M) : ∃ (g : E → F) (φ : ℕ → ℕ), StrictMono φ ∧ DifferentiableOn ℂ g U ∧ TendstoLocallyUniformlyOn (fun (n : ℕ) => f (φ n)) g Filter.atTop U

12. Montel's theorem: a uniformly bounded sequence of holomorphic maps with values in a finite-dimensional space has a locally uniformly convergent subsequence with holomorphic limit.

theorem SCV.vitali {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] [FiniteDimensional ℂ F] {D V : Set E} (hD : IsOpen D) (hconn : IsPreconnected D) {f : ℕ → E → F} (hf : ∀ (n : ℕ), DifferentiableOn ℂ (f n) D) (hb : ∀ K ⊆ D, IsCompact K → ∃ (M : ℝ), ∀ (n : ℕ), ∀ z ∈ K, ‖f n z‖ ≤ M) (hV : IsOpen V) (hne : V.Nonempty) (hVD : V ⊆ D) (hp : ∀ z ∈ V, ∃ (y : F), Filter.Tendsto (fun (n : ℕ) => f n z) Filter.atTop (nhds y)) : ∃ (g : E → F), DifferentiableOn ℂ g D ∧ TendstoLocallyUniformlyOn f g Filter.atTop D

13. Vitali's theorem: a locally bounded sequence of holomorphic maps on a connected open set that converges pointwise on a nonempty open subset converges locally uniformly.

theorem SCV.holomorphic_Lp_bound {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {ι : Type u_3} [Fintype ι] (U : TopologicalSpace.Opens (ι → ℂ)) (p : ENNReal) [Fact (1 ≤ p)] {K : Set (ι → ℂ)} (hKU : K ⊆ ↑U) (hK : IsCompact K) : ∃ (C : ℝ), 0 < C ∧ ∀ (u : ↥(MeasureTheory.Lp F p (MeasureTheory.volume.restrict ↑U))) (f : (ι → ℂ) → F), DifferentiableOn ℂ f ↑U → f =ᵐ[MeasureTheory.volume.restrict ↑U] ↑↑u → ∀ z ∈ K, ‖f z‖ ≤ C * ‖u‖

14. Holomorphic Lᵖ spaces: on compact subsets, a holomorphic representative of an Lᵖ class is bounded by a constant times the Lᵖ norm, for 1 ≤ p ≤ ∞.

C. Local holomorphic mappings

theorem SCV.inverse_mapping {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℂ G] [FiniteDimensional ℂ G] {U : Set E} (hU : IsOpen U) {f : E → G} (hf : DifferentiableOn ℂ f U) {a : E} (ha : a ∈ U) (hinv : (fderiv ℂ f a).IsInvertible) : ∃ (e : OpenPartialHomeomorph E G), DifferentiableOn ℂ (↑e) e.source ∧ DifferentiableOn ℂ (↑e.symm) e.target ∧ a ∈ e.source ∧ e.source ⊆ U ∧ ↑e = f ∧ fderiv ℂ (↑e.symm) (f a) = (fderiv ℂ f a).inverse

15. Holomorphic inverse mapping theorem: a holomorphic map with invertible derivative at a is near a a homeomorphism between open sets that is holomorphic in both directions.

theorem SCV.implicit_mapping {P : Type u_4} {Q : Type u_5} {R : Type u_6} [NormedAddCommGroup P] [NormedSpace ℂ P] [NormedAddCommGroup Q] [NormedSpace ℂ Q] [NormedAddCommGroup R] [NormedSpace ℂ R] [FiniteDimensional ℂ P] [FiniteDimensional ℂ Q] [CompleteSpace R] {D : Set (P × Q)} (hD : IsOpen D) {f : P × Q → R} (hf : DifferentiableOn ℂ f D) {a : P} {b : Q} (hab : (a, b) ∈ D) (hi : (fderiv ℂ f (a, b) ∘SL ContinuousLinearMap.inr ℂ P Q).IsInvertible) : ∃ (U : Set P) (V : Set Q) (g : P → Q), IsOpen U ∧ a ∈ U ∧ IsOpen V ∧ b ∈ V ∧ U ×ˢ V ⊆ D ∧ DifferentiableOn ℂ g U ∧ Set.MapsTo g U V ∧ g a = b ∧ HasFDerivAt g ((-(fderiv ℂ f (a, b) ∘SL ContinuousLinearMap.inr ℂ P Q).inverse) ∘SL fderiv ℂ f (a, b) ∘SL ContinuousLinearMap.inl ℂ P Q) a ∧ ∀ x ∈ U, ∀ y ∈ V, f (x, y) = f (a, b) ↔ y = g x

16. Holomorphic implicit mapping theorem, with the derivative of the implicit map.

D. Reinhardt geometry, power series, and continuation

def SCV.IsReinhardt {ι : Type u_3} (U : Set (ι → ℂ)) : Prop

A set is Reinhardt if it is invariant under independent rotations of the coordinates.

Equations

• SCV.IsReinhardt U = ∀ ⦃z : ι → ℂ⦄, z ∈ U → ∀ ⦃w : ι → ℂ⦄, (∀ (i : ι), ‖w i‖ = ‖z i‖) → w ∈ U

def SCV.IsCompleteReinhardt {ι : Type u_3} (U : Set (ι → ℂ)) : Prop

A set is complete Reinhardt if it is closed under decreasing the coordinate moduli.

Equations

• SCV.IsCompleteReinhardt U = ∀ ⦃z : ι → ℂ⦄, z ∈ U → ∀ ⦃w : ι → ℂ⦄, (∀ (i : ι), ‖w i‖ ≤ ‖z i‖) → w ∈ U

def SCV.IsLogarithmicallyConvex {ι : Type u_3} (U : Set (ι → ℂ)) : Prop

Logarithmic convexity: the image of the points without zero coordinates under z ↦ (log |z₁|, …, log |zₙ|) is convex.

Equations

• SCV.IsLogarithmicallyConvex U = Convex ℝ {x : ι → ℝ | (fun (i : ι) => ↑(Real.exp (x i))) ∈ U}

def SCV.convergenceDomain {ι : Type u_3} [Fintype ι] {G : Type u_4} [NormedAddCommGroup G] (c : MvPowerSeries ι G) : Set (ι → ℂ)

The convergence domain of a power series: the interior of its set of absolute convergence.

Equations

• SCV.convergenceDomain c = interior {z : ι → ℂ | Summable fun (m : ι →₀ ℕ) => ‖c m‖ * ∏ i : ι, ‖z i‖ ^ m i}

theorem SCV.IsCompleteReinhardt.isReinhardt_and_isPathConnected {ι : Type u_3} {U : Set (ι → ℂ)} (hU : IsCompleteReinhardt U) : IsReinhardt U ∧ (U.Nonempty → IsPathConnected U)

17. Complete Reinhardt geometry: a complete Reinhardt set is Reinhardt and, when nonempty, path connected.

theorem SCV.isLogarithmicallyConvex_iff_geometric {ι : Type u_3} [Finite ι] {U : Set (ι → ℂ)} (ho : IsOpen U) (hc : IsCompleteReinhardt U) : IsLogarithmicallyConvex U ↔ ∀ z ∈ U, ∀ w ∈ U, ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → a + b = 1 → ∀ (v : ι → ℂ), (∀ (i : ι), ‖v i‖ = ‖z i‖ ^ a * ‖w i‖ ^ b) → v ∈ U

18. Logarithmic convexity including zero coordinates: for an open complete Reinhardt set, logarithmic convexity is closure under weighted geometric means of the coordinate moduli, with the convention 0 ^ 0 = 1.

theorem SCV.convergenceDomain_properties {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {ι : Type u_3} [Fintype ι] (c : MvPowerSeries ι F) : IsCompleteReinhardt (convergenceDomain c) ∧ IsLogarithmicallyConvex (convergenceDomain c) ∧ AnalyticOnNhd ℂ (fun (z : ι → ℂ) => ∑' (m : ι →₀ ℕ), (∏ i : ι, z i ^ m i) • c m) (convergenceDomain c)

19. Convergence domains of power series are complete Reinhardt and logarithmically convex, and the sum of the series is holomorphic there.

theorem SCV.exists_powerSeries_eqOn_of_isCompleteReinhardt {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {n : ℕ} {U : Set (Fin n → ℂ)} (ho : IsOpen U) (hc : IsCompleteReinhardt U) {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) : ∃ (c : MvPowerSeries (Fin n) F), U ⊆ convergenceDomain c ∧ Set.EqOn (fun (z : Fin n → ℂ) => ∑' (m : Fin n →₀ ℕ), (∏ i : Fin n, z i ^ m i) • c m) f U

20. Taylor representation on complete Reinhardt sets: a holomorphic function on an open complete Reinhardt set is the sum of one power series on the whole set.

theorem SCV.exists_convergenceDomain_eq {ι : Type u_3} [Fintype ι] {U : Set (ι → ℂ)} (hU : IsOpen U) (hne : U.Nonempty) (hc : IsCompleteReinhardt U) (hl : IsLogarithmicallyConvex U) : ∃ (c : MvPowerSeries ι ℂ), convergenceDomain c = U

21. Characterization of convergence domains: every nonempty open complete logarithmically convex Reinhardt set is the convergence domain of a scalar power series.

theorem SCV.existsUnique_laurent_expansion {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {n : ℕ} {U : Set (Fin n → ℂ)} (ho : IsOpen U) (hc : IsPreconnected U) (hne : U.Nonempty) (hR : IsReinhardt U) {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) : ∃! c : (Fin n → ℤ) → F, HasSumLocallyUniformlyOn (fun (m : Fin n → ℤ) (z : Fin n → ℂ) => (∏ i : Fin n, z i ^ m i) • c m) f U

22. Laurent expansion on Reinhardt domains: a holomorphic function on a nonempty connected open Reinhardt set has a unique locally uniformly convergent Laurent expansion.

theorem SCV.exists_extension_completeReinhardtHull {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {n : ℕ} {U : Set (Fin n → ℂ)} (ho : IsOpen U) (hc : IsConnected U) (hR : IsReinhardt U) (hzero : 0 ∈ U) {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) : ∃ (g : (Fin n → ℂ) → F), AnalyticOnNhd ℂ g {w : Fin n → ℂ | ∃ z ∈ U, ∀ (i : Fin n), ‖w i‖ ≤ ‖z i‖} ∧ Set.EqOn g f U

23. Continuation from Reinhardt domains: a holomorphic function on a connected open Reinhardt set containing the origin extends to the complete Reinhardt hull.

theorem SCV.exists_extension_balancedHull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set E} (ho : IsOpen U) (hc : IsPreconnected U) (hrot : ∀ ⦃z : E⦄, z ∈ U → ∀ ⦃c : ℂ⦄, ‖c‖ = 1 → c • z ∈ U) (hzero : 0 ∈ U) {f : E → F} (hf : AnalyticOnNhd ℂ f U) : ∃ (g : E → F), AnalyticOnNhd ℂ g ((balancedHull ℂ) U) ∧ Set.EqOn g f U

24. Continuation from circular domains: a holomorphic function on a connected open set invariant under z ↦ e^{iθ} z and containing the origin extends to the balanced hull.

E. Hartogs phenomena and removable singularities

theorem SCV.hartogs_taylor_expansion {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (E × ℂ)} (hU : IsOpen U) (hH : ∀ ⦃z : E⦄ ⦃w : ℂ⦄, (z, w) ∈ U → ∀ ⦃v : ℂ⦄, ‖v‖ ≤ ‖w‖ → (z, v) ∈ U) {f : E × ℂ → F} (hf : DifferentiableOn ℂ f U) : (∀ (k : ℕ), DifferentiableOn ℂ (fun (z : E) => (↑k.factorial)⁻¹ • iteratedDeriv k (fun (w : ℂ) => f (z, w)) 0) (Prod.fst '' U)) ∧ HasSumLocallyUniformlyOn (fun (k : ℕ) (p : E × ℂ) => p.2 ^ k • (↑k.factorial)⁻¹ • iteratedDeriv k (fun (w : ℂ) => f (p.1, w)) 0) f U

25. Hartogs–Taylor expansion: on an open set U ⊆ E × ℂ whose fibres are closed under decreasing |w|, a holomorphic function is the locally uniform sum of its fibre Taylor series, whose coefficients are holomorphic on the projection of U.

theorem SCV.hartogs_cylinder_extension {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {D D₀ : Set E} (hD : IsOpen D) (hc : IsPreconnected D) (hD₀ : IsOpen D₀) (hne : D₀.Nonempty) (hsub : D₀ ⊆ D) {ρ R : ℝ} (hρ : 0 ≤ ρ) (hρR : ρ < R) {f : E × ℂ → F} (hf : AnalyticOnNhd ℂ f (D ×ˢ (Metric.ball 0 R \ Metric.closedBall 0 ρ) ∪ D₀ ×ˢ Metric.ball 0 R)) : ∃ (g : E × ℂ → F), AnalyticOnNhd ℂ g (D ×ˢ Metric.ball 0 R) ∧ Set.EqOn g f (D ×ˢ (Metric.ball 0 R \ Metric.closedBall 0 ρ) ∪ D₀ ×ˢ Metric.ball 0 R)

26. Hartogs' continuity theorem: a holomorphic function on the union of an annular cylinder over a connected base D and a full cylinder over a nonempty open D₀ ⊆ D extends to the full cylinder over D.

theorem SCV.hartogs_separate_analyticity {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hU : IsOpen U) (hf : ∀ z ∈ U, ∀ (i : ι), AnalyticAt ℂ (fun (w : ℂ) => f (Function.update z i w)) (z i)) : AnalyticOnNhd ℂ f U

27. Hartogs' theorem on separate analyticity: a function on an open subset of ℂ^ι that is analytic in each variable separately is analytic, with no continuity or boundedness hypothesis.

theorem SCV.exists_extension_diff_singleton {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hdim : 2 ≤ Module.finrank ℂ E) {U : Set E} (ho : IsOpen U) {a : E} (ha : a ∈ U) {f : E → F} (hf : AnalyticOnNhd ℂ f (U \ {a})) : ∃ (g : E → F), AnalyticOnNhd ℂ g U ∧ Set.EqOn g f (U \ {a})

28. Isolated singularities are removable in dimension at least two.

theorem SCV.frequently_zero_punctured {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] (hdim : 2 ≤ Module.finrank ℂ E) {f : E → ℂ} {a : E} (hf : AnalyticAt ℂ f a) (ha : f a = 0) : ∃ᶠ (z : E) in nhdsWithin a {a}ᶜ, f z = 0

29. Zeros are not isolated in dimension at least two.

theorem SCV.riemann_extension_first {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set E} (hU : IsOpen U) (hconn : IsPreconnected U) {g : E → ℂ} (hg : AnalyticOnNhd ℂ g U) (hne : ∃ z ∈ U, g z ≠ 0) {f : E → F} (hf : AnalyticOnNhd ℂ f (U \ g ⁻¹' {0})) (hb : ∀ a ∈ U, g a = 0 → ∃ (r : ℝ), 0 < r ∧ ∃ (C : ℝ), ∀ z ∈ Metric.ball a r ∩ (U \ g ⁻¹' {0}), ‖f z‖ ≤ C) : ∃ (f' : E → F), AnalyticOnNhd ℂ f' U ∧ Set.EqOn f' f (U \ g ⁻¹' {0})

30. First Riemann extension theorem: a holomorphic function on the complement of the zero set of a nonzero holomorphic function g on a connected open set, locally bounded near that zero set, extends holomorphically.

theorem SCV.hartogs_compact_hole {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (hdim : 2 ≤ Module.finrank ℂ E) {U K : Set E} (hU : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) (hcompl : IsPreconnected (U \ K)) {f : E → F} (hf : AnalyticOnNhd ℂ f (U \ K)) : ∃ (g : E → F), AnalyticOnNhd ℂ g U ∧ Set.EqOn g f (U \ K)

31. Hartogs' extension theorem (compact holes): in dimension at least two, a holomorphic function on U \ K, with K ⊆ U compact and U \ K connected, extends to U.

F. Elementary analytic sets

def SCV.IsAnalyticSet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U A : Set E) : Prop

A is an analytic subset of U: near every point of U it is the common zero set of finitely many holomorphic functions.

Equations

• One or more equations did not get rendered due to their size.

def SCV.IsRegularAnalyticSetAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : Set E) (a : E) (q : ℕ) : Prop

a is a regular point of A of codimension q: a local biholomorphic change of coordinates carries A to a complex linear subspace of codimension q.

Equations

• One or more equations did not get rendered due to their size.

theorem SCV.IsAnalyticSet.interior_eq_empty_and_isConnected_sdiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U A : Set E} (hA : IsAnalyticSet U A) (hc : IsConnected U) (hp : A ≠ U) : interior A = ∅ ∧ IsConnected (U \ A)

32. Analytic sets are thin: a proper analytic subset of a connected open set has empty interior and connected complement.

theorem SCV.isRegularAnalyticSetAt_iff_exists_equations {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {A : Set E} {a : E} {q : ℕ} : IsRegularAnalyticSetAt A a q ↔ a ∈ A ∧ ∃ (V : Set E) (f : E → Fin q → ℂ), IsOpen V ∧ a ∈ V ∧ AnalyticOnNhd ℂ f V ∧ (∀ z ∈ V, z ∈ A ↔ f z = 0) ∧ Function.Surjective ⇑(fderiv ℂ f a)

33. Regular points and full-rank equations: a is a regular point of codimension q exactly when A is near a the zero set of q holomorphic equations of full rank at a.

theorem SCV.exists_extension_across_coordinatePlane {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set ((E × ℂ) × ℂ)} (hU : IsOpen U) {f : (E × ℂ) × ℂ → F} (hf : AnalyticOnNhd ℂ f (U \ {z : (E × ℂ) × ℂ | z.1.2 = 0 ∧ z.2 = 0})) : ∃ (g : (E × ℂ) × ℂ → F), AnalyticOnNhd ℂ g U ∧ Set.EqOn g f (U \ {z : (E × ℂ) × ℂ | z.1.2 = 0 ∧ z.2 = 0})

34. Removal of a coordinate plane of codimension two.

theorem SCV.riemann_extension_second {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U A : Set E} (hA : IsAnalyticSet U A) (hcodim : ∀ a ∈ A, ∃ (L : (Fin 2 → ℂ) →L[ℂ] E), Function.Injective ⇑L ∧ ∀ᶠ (z : Fin 2 → ℂ) in nhds 0, a + L z ∈ A → z = 0) {f : E → F} (hf : AnalyticOnNhd ℂ f (U \ A)) : ∃ (g : E → F), AnalyticOnNhd ℂ g U ∧ Set.EqOn g f (U \ A)

35. Second Riemann extension theorem: holomorphic functions extend across an analytic subset through each point of which some complex affine plane meets it only at that point, locally.

G. Germs, Weierstrass theory, and elementary local algebra

def SCV.analyticGermRing {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (x : E) : Subring ((nhds x).Germ ℂ)

The ring 𝒪ₓ of germs at x of scalar analytic functions, as a subring of all germs.

Equations

• SCV.analyticGermRing x = { carrier := {φ : (nhds x).Germ ℂ | ∃ (f : E → ℂ), AnalyticAt ℂ f x ∧ ↑f = φ}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def SCV.germ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {x : E} (f : E → ℂ) (hf : AnalyticAt ℂ f x) : ↥(analyticGermRing x)

The germ at x of a function analytic at x.

Equations

• SCV.germ f hf = ⟨↑f, ⋯⟩

def SCV.weierstrassRemainder {E : Type u_1} {d : ℕ} (a : Fin d → E → ℂ) (z : E × ℂ) : ℂ

A remainder of degree less than d in the last variable, with coefficient functions a j.

Equations

• SCV.weierstrassRemainder a z = ∑ j : Fin d, a j z.1 * z.2 ^ ↑j

def SCV.IsWeierstrassDivisionAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {d : ℕ} (f g q : E × ℂ → ℂ) (a : Fin d → E → ℂ) : Prop

Weierstrass division at the origin: g = q f + r as germs, with r a polynomial of degree less than d in the last variable.

Equations

• SCV.IsWeierstrassDivisionAt f g q a = (AnalyticAt ℂ q 0 ∧ (∀ (j : Fin d), AnalyticAt ℂ (a j) 0) ∧ g =ᶠ[nhds 0] fun (z : E × ℂ) => q z * f z + SCV.weierstrassRemainder a z)

def SCV.IsWeierstrassPreparationAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {d : ℕ} (f u : E × ℂ → ℂ) (a : Fin d → E → ℂ) : Prop

Weierstrass preparation at the origin: f = u W as germs, with u a unit and W a distinguished polynomial of degree d in the last variable.

Equations

• One or more equations did not get rendered due to their size.

theorem SCV.analyticGermRing_isDomain_isLocalRing {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (x : E) : IsDomain ↥(analyticGermRing x) ∧ IsLocalRing ↥(analyticGermRing x) ∧ ∀ (f : E → ℂ) (hf : AnalyticAt ℂ f x), IsUnit (germ f hf) ↔ f x ≠ 0

36. The ring of analytic germs is a local integral domain, and a germ is a unit exactly when it does not vanish at the base point.

theorem SCV.exists_regular_coordinate_change {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {f : E × ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (hne : ¬f =ᶠ[nhds 0] 0) : ∃ (L : (E × ℂ) ≃L[ℂ] E × ℂ) (d : ℕ), analyticOrderAt (fun (w : ℂ) => f (L (0, w))) 0 = ↑d

37. Coordinate normalization: after a linear change of coordinates, a nonzero germ has finite order in the last variable.

theorem SCV.taylorSeries_mul_and_eq_zero_iff {n : ℕ} {x : Fin n → ℂ} {f g : (Fin n → ℂ) → ℂ} (hf : AnalyticAt ℂ f x) (hg : AnalyticAt ℂ g x) : taylorSeries (f * g) x = taylorSeries f x * taylorSeries g x ∧ (taylorSeries f x = 0 ↔ f =ᶠ[nhds x] 0)

38. Taylor series determine germs and are multiplicative.

theorem SCV.coordinatePower_division {ι : Type u_3} [Finite ι] (d : ℕ) {r : ι → ℝ} {R : ℝ} (hR : 0 < R) {P : Set (ι → ℂ)} (hP : P = Set.univ.pi fun (i : ι) => Metric.ball 0 (r i)) {g : (ι → ℂ) × ℂ → ℂ} (hg : DifferentiableOn ℂ g (P ×ˢ Metric.ball 0 R)) : ∃ (q : (ι → ℂ) × ℂ → ℂ) (a : Fin d → (ι → ℂ) → ℂ), DifferentiableOn ℂ q (P ×ˢ Metric.ball 0 R) ∧ (∀ (j : Fin d), DifferentiableOn ℂ (a j) P) ∧ Set.EqOn g (fun (z : (ι → ℂ) × ℂ) => q z * z.2 ^ d + weierstrassRemainder a z) (P ×ˢ Metric.ball 0 R) ∧ ∀ (M : ℝ), 0 ≤ M → (∀ z ∈ P ×ˢ Metric.ball 0 R, ‖g z‖ ≤ M) → ∀ z ∈ P ×ˢ Metric.ball 0 R, ‖q z‖ ≤ ↑(d + 1) / R ^ d * M

39. Division by a power of the last coordinate on a product of a polydisc P and a disc, with a bound for the quotient.

theorem SCV.weierstrass_division {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {d : ℕ} {f g : E × ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0) (horder : analyticOrderAt (fun (w : ℂ) => f (0, w)) 0 = ↑d) : ∃ (q : E × ℂ → ℂ) (a : Fin d → E → ℂ), IsWeierstrassDivisionAt f g q a ∧ ∀ (q' : E × ℂ → ℂ) (a' : Fin d → E → ℂ), IsWeierstrassDivisionAt f g q' a' → q =ᶠ[nhds 0] q' ∧ ∀ (j : Fin d), a j =ᶠ[nhds 0] a' j

40. Weierstrass division theorem, with uniqueness of quotient and remainder as germs.

theorem SCV.weierstrass_preparation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {d : ℕ} {f : E × ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (horder : analyticOrderAt (fun (w : ℂ) => f (0, w)) 0 = ↑d) : ∃ (u : E × ℂ → ℂ) (a : Fin d → E → ℂ), IsWeierstrassPreparationAt f u a ∧ ∀ (v : E × ℂ → ℂ) (b : Fin d → E → ℂ), IsWeierstrassPreparationAt f v b → u =ᶠ[nhds 0] v ∧ ∀ (j : Fin d), a j =ᶠ[nhds 0] b j

41. Weierstrass preparation theorem, with uniqueness of the unit and the polynomial.

theorem SCV.analyticGermRing_isNoetherianRing_ufd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] (x : E) : IsNoetherianRing ↥(analyticGermRing x) ∧ UniqueFactorizationMonoid ↥(analyticGermRing x)

44–45. The ring of analytic germs is Noetherian and factorial.

theorem SCV.isOpen_isRelPrime_locus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] (f g : E → ℂ) : IsOpen {x : E | ∃ (hf : AnalyticAt ℂ f x) (hg : AnalyticAt ℂ g x), IsRelPrime (germ f hf) (germ g hg)}

45. Relative primality persists: the set of points at which the germs of two functions are analytic and relatively prime is open.

H. Zero-set geometry and biholomorphic rigidity

theorem SCV.exists_regularPoint_zeroSet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} (hU : IsOpen U) (hc : IsPreconnected U) {f : E → ℂ} (hf : AnalyticOnNhd ℂ f U) (hne : ∃ b ∈ U, f b ≠ 0) (hz : ∃ a ∈ U, f a = 0) : ∃ (a : E), IsRegularAnalyticSetAt (U ∩ f ⁻¹' {0}) a 1

46. Regular points of hypersurfaces: the zero set of a holomorphic function on a connected open set, if nonempty and proper, contains a regular point of codimension one.

theorem SCV.injOn_biholomorphic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℂ G] [FiniteDimensional ℂ G] (hdim : Module.finrank ℂ E = Module.finrank ℂ G) {U : Set E} (hU : IsOpen U) {f : E → G} (hf : DifferentiableOn ℂ f U) (hi : Set.InjOn f U) : ∃ (e : OpenPartialHomeomorph E G), DifferentiableOn ℂ (↑e) e.source ∧ DifferentiableOn ℂ (↑e.symm) e.target ∧ e.source = U ∧ e.target = f '' U ∧ ↑e = f

47. Injective holomorphic maps in equal dimensions are biholomorphic onto their open image.

theorem SCV.cartan_uniqueness {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} (hU : IsOpen U) (hconn : IsPreconnected U) (hb : Bornology.IsBounded U) {f : E → E} (hf : AnalyticOnNhd ℂ f U) (hmaps : Set.MapsTo f U U) {a : E} (ha : a ∈ U) (hfix : f a = a) (hderiv : fderiv ℂ f a = ContinuousLinearMap.id ℂ E) : Set.EqOn f id U

48. Cartan's uniqueness theorem: a holomorphic self-map of a bounded connected open set fixing a point with identity derivative there is the identity.

theorem SCV.biholomorphic_circular_linear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℂ G] [FiniteDimensional ℂ G] {e : OpenPartialHomeomorph E G} (he : DifferentiableOn ℂ (↑e) e.source) (he' : DifferentiableOn ℂ (↑e.symm) e.target) (hc : IsPreconnected e.source) (hb : Bornology.IsBounded e.source) (hrot : ∀ ⦃z : E⦄, z ∈ e.source → ∀ ⦃c : ℂ⦄, ‖c‖ = 1 → c • z ∈ e.source) (hrot' : ∀ ⦃z : G⦄, z ∈ e.target → ∀ ⦃c : ℂ⦄, ‖c‖ = 1 → c • z ∈ e.target) (hzero : 0 ∈ e.source) (hfix : ↑e 0 = 0) : ∃ (L : E ≃L[ℂ] G), Set.EqOn (↑e) (⇑L) e.source

49. Biholomorphisms of circular domains fixing the origin are linear, when the source is bounded and connected.

theorem SCV.exists_ball_automorphism {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {a b : H} (ha : a ∈ Metric.ball 0 1) (hb : b ∈ Metric.ball 0 1) : ∃ (e : OpenPartialHomeomorph H H), DifferentiableOn ℂ (↑e) e.source ∧ DifferentiableOn ℂ (↑e.symm) e.target ∧ e.source = Metric.ball 0 1 ∧ e.target = Metric.ball 0 1 ∧ ↑e a = b

50. The automorphisms of the unit ball of a complex inner product space act transitively.

theorem SCV.not_biholomorphic_polydisc_ball {ι : Type u_3} [Fintype ι] (hdim : 2 ≤ Fintype.card ι) : ¬∃ (e : OpenPartialHomeomorph (ι → ℂ) (EuclideanSpace ℂ ι)), DifferentiableOn ℂ (↑e) e.source ∧ DifferentiableOn ℂ (↑e.symm) e.target ∧ e.source = Metric.ball 0 1 ∧ e.target = Metric.ball 0 1

50. The unit polydisc and the Euclidean unit ball are not biholomorphic in dimension at least two.

I. Common extensions, holomorphic convexity, Cartan–Thullen, and Bochner's tube theorem

def SCV.holomorphicHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U K : Set E) : Set E

The holomorphic hull of K relative to U: the points of U at which every holomorphic function on U is bounded by each of its bounds on K.

Equations

• SCV.holomorphicHull U K = {z : E | z ∈ U ∧ ∀ (f : E → ℂ), AnalyticOnNhd ℂ f U → ∀ (M : ℝ), (∀ w ∈ K, ‖f w‖ ≤ M) → ‖f z‖ ≤ M}

def SCV.IsHolomorphicallyConvex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) : Prop

U is holomorphically convex: hulls of compact subsets are compact.

Equations

• SCV.IsHolomorphicallyConvex U = ∀ (K : Set E), IsCompact K → K ⊆ U → IsCompact (SCV.holomorphicHull U K)

def SCV.IsDomainOfHolomorphy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) : Prop

The generalized domain-of-holomorphy continuation property for a set U: there is no connected open set V ⊄ U with a nonempty open W ⊆ U ∩ V such that every holomorphic function on U agrees on W with one on V.

Openness, connectedness, and nonemptiness of U are separate hypotheses. This predicate is automatically satisfied when interior U = ∅, because no nonempty open overlap exists.

Equations

• One or more equations did not get rendered due to their size.

def SCV.IsDomainOfExistence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) (f : E → ℂ) : Prop

U is the domain of existence of f: f is holomorphic on U and has no continuation in the above sense.

Equations

• One or more equations did not get rendered due to their size.

theorem SCV.common_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : Set E} (hUV : U ⊆ V) (hext : ∀ (f : E → ℂ), AnalyticOnNhd ℂ f U → ∃ (g : E → ℂ), AnalyticOnNhd ℂ g V ∧ Set.EqOn g f U) (ho : IsOpen U) (hne : U.Nonempty) (hc : IsPreconnected V) : V ⊆ (convexHull ℝ) U ∧ ∀ (f : E → ℂ), AnalyticOnNhd ℂ f V → f '' V = f '' U

51. Common extension domains: if every holomorphic function on a nonempty open U extends to the connected set V ⊇ U, then V lies in the convex hull of U and holomorphic functions on V take no new values.

theorem SCV.holomorphicHull_idem_and_isBounded {ι : Type u_3} [Fintype ι] (U : Set (ι → ℂ)) {K : Set (ι → ℂ)} : holomorphicHull U (holomorphicHull U K) = holomorphicHull U K ∧ (Bornology.IsBounded K → Bornology.IsBounded (holomorphicHull U K))

52. Holomorphic hulls are idempotent, and hulls of bounded sets are bounded.

theorem SCV.isHolomorphicallyConvex_of_completeReinhardt {ι : Type u_3} [Fintype ι] {U : Set (ι → ℂ)} (ho : IsOpen U) (hc : IsCompleteReinhardt U) (hl : IsLogarithmicallyConvex U) : IsHolomorphicallyConvex U

52. Open complete logarithmically convex Reinhardt sets are holomorphically convex.

theorem SCV.isDomainOfHolomorphy_of_convex_and_pi {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ι : Type u_3} [Fintype ι] : (∀ (U : Set E), Convex ℝ U → IsOpen U → IsDomainOfHolomorphy U) ∧ ∀ (S : ι → Set ℂ), IsDomainOfHolomorphy (Set.univ.pi S)

53. Elementary continuation obstructions. Convex open sets and finite products of arbitrary plane sets satisfy IsDomainOfHolomorphy, the continuation-obstruction predicate defined above. This predicate does not require openness, connectedness, or nonemptiness. It holds vacuously whenever the set has empty interior, because no nonempty open overlap exists. For nonempty connected open plane factors, the product assertion recovers the classical theorem that their product is a domain of holomorphy.

theorem SCV.isHolomorphicallyConvex_iff_escaping {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} (ho : IsOpen U) : IsHolomorphicallyConvex U ↔ ∀ (p : ℕ → E), (∀ (j : ℕ), p j ∈ U) → (∀ (K : Set E), IsCompact K → K ⊆ U → ∀ᶠ (j : ℕ) in Filter.atTop, p j ∉ K) → ∃ (f : E → ℂ), AnalyticOnNhd ℂ f U ∧ ¬BddAbove (Set.range fun (j : ℕ) => ‖f (p j)‖)

54. Escaping sequences: an open set is holomorphically convex exactly when every sequence leaving all its compact subsets is unbounded under some holomorphic function.

theorem SCV.isDomainOfHolomorphy_iff_hull_radius {n : ℕ} {U : Set (Fin n → ℂ)} (ho : IsOpen U) : IsDomainOfHolomorphy U ↔ ∀ (K : Set (Fin n → ℂ)), IsCompact K → K ⊆ U → ∀ (r : ℝ), 0 < r → (∀ x ∈ K, Metric.ball x r ⊆ U) → ∀ a ∈ holomorphicHull U K, Metric.ball a r ⊆ U

55. Thullen's lemma, as a characterization: an open subset of ℂ^ι with the supremum norm is a domain of holomorphy exactly when polydisc radii available on a compact set remain available on its holomorphic hull.

theorem SCV.cartan_thullen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} (ho : IsOpen U) : (IsDomainOfHolomorphy U ↔ IsHolomorphicallyConvex U) ∧ (IsDomainOfHolomorphy U ↔ ∃ (f : E → ℂ), IsDomainOfExistence U f)

56. Cartan–Thullen theorem: for an open set, being a domain of holomorphy, holomorphic convexity, and being the domain of existence of one function are equivalent.

theorem SCV.bochner_tube {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {ι : Type u_3} [Fintype ι] {Ω : Set (ι → ℝ)} (ho : IsOpen Ω) (hc : IsPreconnected Ω) : (∀ (f : (ι → ℂ) → F), AnalyticOnNhd ℂ f {z : ι → ℂ | (fun (i : ι) => (z i).re) ∈ Ω} → ∃ (g : (ι → ℂ) → F), AnalyticOnNhd ℂ g {z : ι → ℂ | (fun (i : ι) => (z i).re) ∈ (convexHull ℝ) Ω} ∧ Set.EqOn g f {z : ι → ℂ | (fun (i : ι) => (z i).re) ∈ Ω}) ∧ (IsDomainOfHolomorphy {z : ι → ℂ | (fun (i : ι) => (z i).re) ∈ Ω} ↔ Convex ℝ Ω)

57. Bochner's tube theorem: a holomorphic function on the tube over a connected open base Ω ⊆ ℝ^ι extends to the tube over the convex hull of Ω, and the tube is a domain of holomorphy exactly when Ω is convex.

J. Plurisubharmonic functions, the Levi form, and pseudoconvexity

def SCV.HasSubmeanAt (u : ℂ → ℝ) (a : ℂ) : Prop

The local submean property of u at a: on all small circles around a, u is integrable and u a is at most its average.

Equations

• SCV.HasSubmeanAt u a = ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), CircleIntegrable u a r ∧ u a ≤ Real.circleAverage u a r

def SCV.SubharmonicOn (u : ℂ → ℝ) (U : Set ℂ) : Prop

u is subharmonic on U: upper semicontinuous with the local submean property.

Equations

• SCV.SubharmonicOn u U = (UpperSemicontinuousOn u U ∧ ∀ a ∈ U, SCV.HasSubmeanAt u a)

def SCV.PlurisubharmonicOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : E → ℝ) (U : Set E) : Prop

f is plurisubharmonic on U: upper semicontinuous, and subharmonic on every complex line.

Equations

• SCV.PlurisubharmonicOn f U = (UpperSemicontinuousOn f U ∧ ∀ a ∈ U, ∀ (w : E), SCV.SubharmonicOn (fun (t : ℂ) => f (a + t • w)) {t : ℂ | a + t • w ∈ U})

noncomputable def SCV.leviForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : E → ℝ) (a w : E) : ℝ

The Levi form of f at a in the direction w, through the real second derivative.

Equations

• SCV.leviForm f a w = ((iteratedFDeriv ℝ 2 f a) ![w, w] + (iteratedFDeriv ℝ 2 f a) ![Complex.I • w, Complex.I • w]) / 4

def SCV.IsPseudoconvex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) : Prop

U is pseudoconvex: open, with a continuous plurisubharmonic exhaustion function.

Equations

• SCV.IsPseudoconvex U = (IsOpen U ∧ ∃ (φ : E → ℝ), ContinuousOn φ U ∧ SCV.PlurisubharmonicOn φ U ∧ ∀ (c : ℝ), IsCompact {z : E | z ∈ U ∧ φ z ≤ c})

def SCV.IsLocalDefiningFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) (p : E) (ρ : E → ℝ) (V : Set E) : Prop

ρ is a local C² defining function of U on the neighbourhood V of the point p.

Equations

• SCV.IsLocalDefiningFunction U p ρ V = (IsOpen V ∧ p ∈ V ∧ ContDiffOn ℝ 2 ρ V ∧ ρ p = 0 ∧ fderiv ℝ ρ p ≠ 0 ∧ U ∩ V = {z : E | ρ z < 0} ∩ V)

def SCV.IsComplexTangent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (ρ : E → ℝ) (p w : E) : Prop

w is a complex tangent vector at p of the level set of ρ.

Equations

• SCV.IsComplexTangent ρ p w = ((fderiv ℝ ρ p) w = 0 ∧ (fderiv ℝ ρ p) (Complex.I • w) = 0)

def SCV.IsLeviPseudoconvexAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) (p : E) : Prop

The Levi condition at p: for every local defining function, the Levi form is positive semidefinite on the complex tangent space.

Equations

• SCV.IsLeviPseudoconvexAt U p = ∀ (ρ : E → ℝ) (V : Set E), SCV.IsLocalDefiningFunction U p ρ V → ∀ (w : E), SCV.IsComplexTangent ρ p w → 0 ≤ SCV.leviForm ρ p w

theorem SCV.SubharmonicOn.eqOn_const_of_isMaxOn {u : ℂ → ℝ} {U : Set ℂ} {a : ℂ} (hU : IsOpen U) (hc : IsPreconnected U) (hu : SubharmonicOn u U) (ha : a ∈ U) (hmax : ∀ z ∈ U, u z ≤ u a) (z : ℂ) : z ∈ U → u z = u a

58. Maximum principle for subharmonic functions.

theorem SCV.subharmonicOn_iff_laplacian_nonneg {g : ℂ → ℝ} {U : Set ℂ} (hU : IsOpen U) (hg : ContDiffOn ℝ 2 g U) : SubharmonicOn g U ↔ ∀ t ∈ U, 0 ≤ Laplacian.laplacian g t

59. Laplacian criterion: a C² function on an open subset of ℂ is subharmonic exactly when its Laplacian is nonnegative.

theorem SCV.plurisubharmonicOn_iff_leviForm_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℝ} {U : Set E} (hU : IsOpen U) (hf : ContDiffOn ℝ 2 f U) : PlurisubharmonicOn f U ↔ ∀ a ∈ U, ∀ (w : E), 0 ≤ leviForm f a w

60. Levi-form criterion: a C² function is plurisubharmonic exactly when its Levi form is positive semidefinite.

theorem SCV.IsDomainOfHolomorphy.isPseudoconvex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} (hU : IsDomainOfHolomorphy U) (ho : IsOpen U) : IsPseudoconvex U

61. Domains of holomorphy are pseudoconvex.

theorem SCV.IsPseudoconvex.continuity_principle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} (h : IsPseudoconvex U) (a b : ℝ → E) (ha : Continuous a) (hb : Continuous b) (hbdry : ∀ t ∈ Set.Icc 0 1, ∀ ζ ∈ Metric.sphere 0 1, a t + ζ • b t ∈ U) (hinit : ∀ ζ ∈ Metric.closedBall 0 1, a 0 + ζ • b 0 ∈ U) (t : ℝ) : t ∈ Set.Icc 0 1 → ∀ ζ ∈ Metric.closedBall 0 1, a t + ζ • b t ∈ U

61. Pseudoconvex sets satisfy the continuity principle for continuous families of affine analytic discs.

theorem SCV.IsDomainOfHolomorphy.isLeviPseudoconvexAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} (hU : IsDomainOfHolomorphy U) (ho : IsOpen U) {p : E} (hp : p ∈ frontier U) : IsLeviPseudoconvexAt U p

62. Levi's theorem: a domain of holomorphy satisfies the Levi condition at every boundary point admitting a local C² defining function.

theorem SCV.leviForm_comp_analytic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G] {g : G → ℝ} {Φ : E → G} {a : E} (hg : ContDiffAt ℝ 2 g (Φ a)) (hΦ : AnalyticAt ℂ Φ a) (w : E) : leviForm (g ∘ Φ) a w = leviForm g (Φ a) ((fderiv ℂ Φ a) w)

63. The Levi form under holomorphic maps.

theorem SCV.isLeviPseudoconvexAt_iff_of_defining {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {p : E} {ρ : E → ℝ} {V : Set E} (h : IsLocalDefiningFunction U p ρ V) : IsLeviPseudoconvexAt U p ↔ ∀ (w : E), IsComplexTangent ρ p w → 0 ≤ leviForm ρ p w

64. Independence of the defining function: the Levi condition may be tested on one local defining function.

theorem SCV.exists_local_peak_function {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} {p : E} {ρ : E → ℝ} {V : Set E} (h : IsLocalDefiningFunction U p ρ V) (hstrict : ∀ (w : E), IsComplexTangent ρ p w → w ≠ 0 → 0 < leviForm ρ p w) : ∃ W ∈ nhds p, ∃ (f : E → ℂ), AnalyticOnNhd ℂ f Set.univ ∧ f p = 1 ∧ ∀ z ∈ W, z ≠ p → ρ z ≤ 0 → ‖f z‖ < 1

64. Local peak functions at strictly Levi pseudoconvex boundary points.

K. Runge domains and polynomial hulls

def SCV.polynomialHull {n : ℕ} (K : Set (Fin n → ℂ)) : Set (Fin n → ℂ)

The polynomial hull of K.

Equations

• SCV.polynomialHull K = {z : Fin n → ℂ | ∀ (P : MvPolynomial (Fin n) ℂ) (M : ℝ), (∀ w ∈ K, ‖(MvPolynomial.eval w) P‖ ≤ M) → ‖(MvPolynomial.eval z) P‖ ≤ M}

def SCV.IsRungeDomain {n : ℕ} (U : Set (Fin n → ℂ)) : Prop

U is a Runge domain: holomorphic functions on U are approximated by polynomials, uniformly on compact subsets.

Equations

• One or more equations did not get rendered due to their size.

theorem SCV.runge_domains {n : ℕ} {U : Set (Fin n → ℂ)} (ho : IsOpen U) : (IsCompleteReinhardt U → IsRungeDomain U) ∧ (IsRungeDomain U → ∀ (K : Set (Fin n → ℂ)), IsCompact K → K ⊆ U → polynomialHull K ∩ U = holomorphicHull U K)

65. Runge domains: open complete Reinhardt sets are Runge domains, and in a Runge domain the polynomial hull of a compact subset meets the domain in its holomorphic hull.