Holomorphic maps with the compact-open topology

Holomorphic maps on an open domain form a closed complex submodule of the continuous maps on that domain. The topology and uniformity are inherited from Mathlib's continuous-map space, not from a global sup norm. In particular, the space is complete for Banach targets.

The zero extension below is only a device for expressing AnalyticOnNhd on the ambient space. No continuity or analyticity at the boundary of the domain is asserted.

noncomputable def CarlsonFunctions.SeveralComplexVariables.openExtension {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (U : TopologicalSpace.Opens (ι → ℂ)) (f : C(↥U, F)) (z : ι → ℂ) : F

Extend a continuous map on an open domain by zero; used only for local analytic predicates.

Equations

• CarlsonFunctions.SeveralComplexVariables.openExtension U f z = if hz : z ∈ U then f ⟨z, hz⟩ else 0

theorem CarlsonFunctions.SeveralComplexVariables.openExtension_apply {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (U : TopologicalSpace.Opens (ι → ℂ)) (f : C(↥U, F)) {z : ι → ℂ} (hz : z ∈ U) : openExtension U f z = f ⟨z, hz⟩

@[simp]

theorem CarlsonFunctions.SeveralComplexVariables.openExtension_coe {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (U : TopologicalSpace.Opens (ι → ℂ)) (f : C(↥U, F)) (z : ↥U) : openExtension U f ↑z = f z

def CarlsonFunctions.SeveralComplexVariables.holomorphicSubmodule {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (U : TopologicalSpace.Opens (ι → ℂ)) : Submodule ℂ C(↥U, F)

Holomorphic maps are a submodule of continuous maps on the open domain.

Equations

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

@[reducible, inline]

abbrev CarlsonFunctions.SeveralComplexVariables.HolomorphicMap {ι : Type u_1} [Fintype ι] (U : TopologicalSpace.Opens (ι → ℂ)) (F : Type u_3) [NormedAddCommGroup F] [NormedSpace ℂ F] : Type (max u_1 u_3)

Holomorphic maps on an open domain, with the induced compact-open topology and uniformity.

Equations

• CarlsonFunctions.SeveralComplexVariables.HolomorphicMap U F = ↥(CarlsonFunctions.SeveralComplexVariables.holomorphicSubmodule U)

theorem CarlsonFunctions.SeveralComplexVariables.tendsto_iff_openExtension {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [Finite ι] {U : TopologicalSpace.Opens (ι → ℂ)} {κ : Type u_3} {l : Filter κ} {f : κ → C(↥U, F)} {g : C(↥U, F)} : Filter.Tendsto f l (nhds g) ↔ TendstoLocallyUniformlyOn (fun (n : κ) => openExtension U (f n)) (openExtension U g) l ↑U

Convergence in the continuous-map space is exactly locally uniform convergence of the ambient extensions on the open domain.

theorem CarlsonFunctions.SeveralComplexVariables.isClosed_holomorphicSubmodule {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (U : TopologicalSpace.Opens (ι → ℂ)) : IsClosed ↑(holomorphicSubmodule U)

Weierstrass convergence makes the holomorphic submodule closed.

instance CarlsonFunctions.SeveralComplexVariables.instCompleteSpaceHolomorphicMap {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (U : TopologicalSpace.Opens (ι → ℂ)) : CompleteSpace (HolomorphicMap U F)

The compact-open uniform space of holomorphic maps into a Banach space is complete.

theorem CarlsonFunctions.SeveralComplexVariables.continuous_holomorphicMap_eval {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] (U : TopologicalSpace.Opens (ι → ℂ)) (z : ↥U) : Continuous fun (f : HolomorphicMap U F) => ↑f z

Evaluation at a point is continuous in the compact-open topology.

theorem CarlsonFunctions.SeveralComplexVariables.holomorphicMap_tendsto_iff {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {U : TopologicalSpace.Opens (ι → ℂ)} {κ : Type u_3} {l : Filter κ} {f : κ → HolomorphicMap U F} {g : HolomorphicMap U F} : Filter.Tendsto f l (nhds g) ↔ TendstoLocallyUniformlyOn (fun (n : κ) => openExtension U ↑(f n)) (openExtension U ↑g) l ↑U

The inherited topology on holomorphic maps is precisely locally uniform convergence.

noncomputable def CarlsonFunctions.SeveralComplexVariables.holomorphicPartialDeriv {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (U : TopologicalSpace.Opens (ι → ℂ)) (i : ι) (f : HolomorphicMap U F) : HolomorphicMap U F

Coordinate differentiation as an operator on holomorphic maps.

Equations

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

theorem CarlsonFunctions.SeveralComplexVariables.continuous_holomorphicPartialDeriv {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (U : TopologicalSpace.Opens (ι → ℂ)) (i : ι) : Continuous (holomorphicPartialDeriv U i)

Coordinate differentiation is continuous for the compact-open topology.

noncomputable def CarlsonFunctions.SeveralComplexVariables.holomorphicRestrict {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {U V : TopologicalSpace.Opens (ι → ℂ)} (hVU : V ≤ U) (f : HolomorphicMap U F) : HolomorphicMap V F

Restriction to a smaller open domain preserves holomorphy.

Equations

• CarlsonFunctions.SeveralComplexVariables.holomorphicRestrict hVU f = ⟨(↑f).comp { toFun := fun (z : ↥V) => ⟨↑z, ⋯⟩, continuous_toFun := ⋯ }, ⋯⟩

theorem CarlsonFunctions.SeveralComplexVariables.continuous_holomorphicRestrict {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {U V : TopologicalSpace.Opens (ι → ℂ)} (hVU : V ≤ U) : Continuous (holomorphicRestrict hVU)

Restriction is continuous for the compact-open topology.