Complex slices and removal in codimension at least two

Following [Scheidemann][Scheidemann2005] §4.1, codimension at least q is expressed by an injective complex linear q-plane on which each point of the subset is an isolated intersection. We retain the pointwise slice witness instead of introducing a general dimension theory. The empty set satisfies every bound; at a point the bound cannot exceed ambient dimension.

Hartogs figures around isolated two-dimensional slices give local holomorphic extensions, and hence automatic local boundedness across the analytic set. The first Riemann extension theorem then gives the global second Riemann extension theorem. Reference: [Scheidemann][Scheidemann2005] 4.1.4 and 4.2.3.

Main definitions

• HasIsolatedComplexSlice: An affine complex q-plane through a meets A only at a near that point.
• HasComplexSliceCodimensionAtLeast: The slice formulation of complex codimension at least q, at every point of A.

Main results

• IsAnalyticSet.locally_bounded_of_codimension_two: Automatic local boundedness in codimension at least two. Hartogs continuation around isolated two-dimensional slices gives a local holomorphic extension, whose continuity supplies the bound.
• IsAnalyticSet.exists_extension_of_codimension_two: Second Riemann extension theorem. No boundedness or connectedness assumption is imposed.

References

• [V. Scheidemann, Introduction to Complex Analysis in Several Variables][Scheidemann2005]

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

An affine complex q-plane through a meets A only at a near that point. Membership of a in A is separate, so this predicate also applies outside A.

Equations

• SeveralComplexVariables.HasIsolatedComplexSlice A a q = ∃ (L : (Fin q → ℂ) →L[ℂ] E), Function.Injective ⇑L ∧ ∀ᶠ (z : Fin q → ℂ) in nhds 0, a + L z ∈ A → z = 0

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

The slice formulation of complex codimension at least q, at every point of A. Analyticity is a separate assumption.

Equations

• SeveralComplexVariables.HasComplexSliceCodimensionAtLeast A q = ∀ a ∈ A, SeveralComplexVariables.HasIsolatedComplexSlice A a q

theorem SeveralComplexVariables.hasComplexSliceCodimensionAtLeast_empty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (q : ℕ) : HasComplexSliceCodimensionAtLeast ∅ q

The empty set satisfies every slice-codimension bound.

theorem SeveralComplexVariables.hasComplexSliceCodimensionAtLeast_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (A : Set E) : HasComplexSliceCodimensionAtLeast A 0

Every subset has slice codimension at least zero; the zero-dimensional slice is a point.

theorem SeveralComplexVariables.HasIsolatedComplexSlice.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {A B : Set E} {a : E} {q : ℕ} (h : HasIsolatedComplexSlice A a q) (hBA : B ⊆ A) : HasIsolatedComplexSlice B a q

Isolated slice intersections are preserved on subsets.

theorem SeveralComplexVariables.HasComplexSliceCodimensionAtLeast.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {A B : Set E} {q : ℕ} (h : HasComplexSliceCodimensionAtLeast A q) (hBA : B ⊆ A) : HasComplexSliceCodimensionAtLeast B q

Slice-codimension bounds pass to subsets, in particular to restrictions to open sets.

theorem SeveralComplexVariables.HasIsolatedComplexSlice.le_finrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {A : Set E} {a : E} {q : ℕ} (h : HasIsolatedComplexSlice A a q) : q ≤ Module.finrank ℂ E

A slice cannot have larger dimension than the ambient finite-dimensional space.

theorem SeveralComplexVariables.HasComplexSliceCodimensionAtLeast.eq_empty_of_finrank_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {A : Set E} {q : ℕ} (h : HasComplexSliceCodimensionAtLeast A q) (hq : Module.finrank ℂ E < q) : A = ∅

A codimension bound exceeding ambient dimension forces the set to be empty.

theorem SeveralComplexVariables.HasIsolatedComplexSlice.notMem_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {A : Set E} {a : E} {q : ℕ} (h : HasIsolatedComplexSlice A a q) (hq : 0 < q) : a ∉ interior A

A positive-dimensional isolated slice excludes an interior point.

theorem SeveralComplexVariables.HasComplexSliceCodimensionAtLeast.interior_eq_empty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {A : Set E} {q : ℕ} (h : HasComplexSliceCodimensionAtLeast A q) (hq : 0 < q) : interior A = ∅

Positive slice codimension implies empty interior, also on disconnected domains.

theorem SeveralComplexVariables.IsAnalyticSet.locally_bounded_of_codimension_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U A : Set E} (hA : IsAnalyticSet U A) (hcodim : HasComplexSliceCodimensionAtLeast A 2) {f : E → F} (hf : AnalyticOnNhd ℂ f (U \ A)) (a : E) : a ∈ A → ∃ (r : ℝ), 0 < r ∧ ∃ (C : ℝ), ∀ z ∈ Metric.ball a r ∩ (U \ A), ‖f z‖ ≤ C

Automatic local boundedness in codimension at least two. Hartogs continuation around isolated two-dimensional slices gives a local holomorphic extension, whose continuity supplies the bound. This allows arbitrary complex Banach targets.

theorem SeveralComplexVariables.IsAnalyticSet.exists_extension_of_codimension_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U A : Set E} (hA : IsAnalyticSet U A) (hcodim : HasComplexSliceCodimensionAtLeast A 2) {f : E → F} (hf : AnalyticOnNhd ℂ f (U \ A)) : ∃ (g : E → F), AnalyticOnNhd ℂ g U ∧ Set.EqOn g f (U \ A)

Second Riemann extension theorem. No boundedness or connectedness assumption is imposed. The proof depends on automatic local boundedness in codimension two.

theorem SeveralComplexVariables.IsAnalyticSet.extension_unique_of_codimension_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type u_2} [TopologicalSpace F] [T2Space F] {U A : Set E} (hA : IsAnalyticSet U A) (hcodim : HasComplexSliceCodimensionAtLeast A 2) {f g h : E → F} (hg : ContinuousOn g U) (hh : ContinuousOn h U) (hgf : Set.EqOn g f (U \ A)) (hhf : Set.EqOn h f (U \ A)) : Set.EqOn g h U

Extensions in the second Riemann theorem are unique on the ambient domain. This uniqueness proof uses density and does not require the existence argument.