Analyticity of holomorphic maps in finite dimension

This file proves the several-complex-variables theorem that a complex Fréchet-differentiable map on an open subset of a finite-dimensional complex normed space is analytic. The general theorem uses coordinates only inside its proof. The file is a temporary project home for material ultimately intended for a Mathlib location such as Mathlib.Analysis.Complex.SeveralVariables.Basic.

Main results

DifferentiableOn.analyticOnNhd_finiteDimensional and differentiableOn_iff_analyticOnNhd_finiteDimensional give the coordinate-free interface for arbitrary finite-dimensional complex normed domains and complete complex normed codomains.

DifferentiableOn.analyticOnNhd_pi and differentiableOn_iff_analyticOnNhd_pi give the corresponding interface for finite coordinate spaces ι → ℂ. Such spaces are natural for separate holomorphy, coordinate derivatives, and polydisc expansions. The coordinate theorem is proved first and then transported along a linear equivalence; this proof order imposes no choice of coordinates on the general statements.

theorem DifferentiableOn.analyticOnNhd_piCarlson {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) : AnalyticOnNhd ℂ f U

A complex Fréchet-differentiable map on an open subset of a finite complex coordinate space is analytic there.

theorem differentiableOn_iff_analyticOnNhd_piCarlson {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hU : IsOpen U) : DifferentiableOn ℂ f U ↔ AnalyticOnNhd ℂ f U

On an open subset of a finite complex coordinate space, complex Fréchet differentiability and analyticity are equivalent.

theorem DifferentiableOn.analyticOnNhd_finiteDimensionalCarlson {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} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) : AnalyticOnNhd ℂ f U

Complex differentiability on an open finite-dimensional domain implies analyticity. No choice of coordinates occurs in the statement.

theorem differentiableOn_iff_analyticOnNhd_finiteDimensionalCarlson {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

On an open finite-dimensional domain, holomorphy may be expressed using either complex Fréchet differentiability or Mathlib's analytic predicate.

theorem Differentiable.analyticOnNhd_finiteDimensionalCarlson {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {f : E → F} (hf : Differentiable ℂ f) : AnalyticOnNhd ℂ f Set.univ

An everywhere complex-differentiable map on a finite-dimensional space is entire.