Locally uniform limits of analytic maps in several variables

This file proves the Weierstrass convergence theorem for finite-dimensional complex domains, its normally summable series consequences, and locally uniform convergence of all mixed coordinate and iterated Fréchet derivatives. The topological notion TendstoLocallyUniformlyOn is Mathlib's.

This is a temporary project home for material ultimately intended for a Mathlib location such as Mathlib.Analysis.Complex.SeveralVariables.LocallyUniform.

Main results

• TendstoLocallyUniformlyOn.analyticOnNhd_pi is the several-variable Weierstrass convergence theorem for finite complex coordinate spaces.
• HasSumLocallyUniformlyOn.analyticOnNhd_pi is its series form.
• TendstoLocallyUniformlyOn.partialDeriv and TendstoLocallyUniformlyOn.iteratedPartialDeriv give convergence of coordinate derivatives.
• HasSumLocallyUniformlyOn.iteratedPartialDeriv gives termwise differentiation of series.
• TendstoLocallyUniformlyOn.analyticOnNhd_finiteDimensional and TendstoLocallyUniformlyOn.iteratedFDeriv_finiteDimensional are the coordinate-independent formulations, with multilinear operator norm for the latter.

Derivative convergence uses a one-variable Cauchy estimate on compact thickenings, followed by finite sums, currying, and transport along a continuous linear choice of coordinates.

theorem TendstoLocallyUniformlyOn.analyticOnNhd_piCarlson {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {l : Filter κ} [l.NeBot] {f : κ → (ι → ℂ) → F} {g : (ι → ℂ) → F} (hlim : TendstoLocallyUniformlyOn f g l U) (hf : ∀ᶠ (n : κ) in l, AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) : AnalyticOnNhd ℂ g U

Weierstrass convergence theorem, finite-coordinate form. A locally uniform limit of analytic maps on an open subset of a finite complex coordinate space is analytic.

theorem HasSumLocallyUniformlyOn.analyticOnNhd_piCarlson {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : κ → (ι → ℂ) → F} {g : (ι → ℂ) → F} (hsum : HasSumLocallyUniformlyOn f g U) (hf : ∀ (n : κ), AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) : AnalyticOnNhd ℂ g U

A locally uniformly convergent sum of analytic maps on an open finite complex coordinate space is analytic.

theorem analyticOnNhd_tsum_of_summable_norm_on_compactsCarlson {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : κ → (ι → ℂ) → F} (hU : IsOpen U) (hf : ∀ (n : κ), AnalyticOnNhd ℂ (f n) U) (hmajorant : ∀ K ⊆ U, IsCompact K → ∃ (M : κ → ℝ), Summable M ∧ ∀ (n : κ), ∀ x ∈ K, ‖f n x‖ ≤ M n) : AnalyticOnNhd ℂ (fun (x : ι → ℂ) => ∑' (n : κ), f n x) U

A series of analytic maps is analytic when its terms admit a summable uniform majorant on every compact subset of the domain.

theorem TendstoLocallyUniformlyOn.partialDerivCarlson {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {l : Filter κ} [l.NeBot] {f : κ → (ι → ℂ) → F} {g : (ι → ℂ) → F} (hlim : TendstoLocallyUniformlyOn f g l U) (hf : ∀ᶠ (n : κ) in l, AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) (i : ι) : TendstoLocallyUniformlyOn (fun (n : κ) => CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson i (f n)) (CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson i g) l U

Locally uniform convergence of holomorphic maps implies locally uniform convergence of each coordinate derivative. The Cauchy estimate is applied on a compact thickening.

theorem TendstoLocallyUniformlyOn.iteratedPartialDerivCarlson {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {l : Filter κ} [l.NeBot] {f : κ → (ι → ℂ) → F} {g : (ι → ℂ) → F} (hlim : TendstoLocallyUniformlyOn f g l U) (hf : ∀ᶠ (n : κ) in l, AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) (is : List ι) : TendstoLocallyUniformlyOn (fun (n : κ) => CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson is (f n)) (CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson is g) l U

All mixed coordinate derivatives converge locally uniformly on the original domain.

theorem TendstoLocallyUniformlyOn.fderiv_piCarlson {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {l : Filter κ} [l.NeBot] {f : κ → (ι → ℂ) → F} {g : (ι → ℂ) → F} (hlim : TendstoLocallyUniformlyOn f g l U) (hf : ∀ᶠ (n : κ) in l, AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) : TendstoLocallyUniformlyOn (fun (n : κ) => fderiv ℂ (f n)) (fderiv ℂ g) l U

Locally uniform convergence of holomorphic maps gives locally uniform convergence of their Fréchet derivatives in operator norm.

theorem TendstoLocallyUniformlyOn.iteratedFDeriv_piCarlson {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {l : Filter κ} [l.NeBot] {f : κ → (ι → ℂ) → F} {g : (ι → ℂ) → F} (hlim : TendstoLocallyUniformlyOn f g l U) (hf : ∀ᶠ (n : κ) in l, AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) (k : ℕ) : TendstoLocallyUniformlyOn (fun (n : κ) => iteratedFDeriv ℂ k (f n)) (iteratedFDeriv ℂ k g) l U

All iterated Fréchet derivatives converge locally uniformly in multilinear operator norm.

theorem HasSumLocallyUniformlyOn.iteratedPartialDerivCarlson {ι : Type u_1} {κ : Type u_2} {F : Type u_3} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : κ → (ι → ℂ) → F} {g : (ι → ℂ) → F} (hsum : HasSumLocallyUniformlyOn f g U) (hf : ∀ (n : κ), AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) (is : List ι) : HasSumLocallyUniformlyOn (fun (n : κ) => CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson is (f n)) (CarlsonFunctions.SeveralComplexVariables.iteratedPartialDerivCarlson is g) U

A locally uniformly convergent holomorphic series may be differentiated term by term any finite number of times, with locally uniform convergence of the differentiated series.

theorem TendstoLocallyUniformlyOn.analyticOnNhd_finiteDimensionalCarlson {κ : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} {l : Filter κ} [l.NeBot] {f : κ → E → F} {g : E → F} (hlim : TendstoLocallyUniformlyOn f g l U) (hf : ∀ᶠ (n : κ) in l, AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) : AnalyticOnNhd ℂ g U

The Weierstrass convergence theorem on any finite-dimensional complex normed domain.

theorem TendstoLocallyUniformlyOn.fderiv_finiteDimensionalCarlson {κ : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} {l : Filter κ} [l.NeBot] {f : κ → E → F} {g : E → F} (hlim : TendstoLocallyUniformlyOn f g l U) (hf : ∀ᶠ (n : κ) in l, AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) : TendstoLocallyUniformlyOn (fun (n : κ) => fderiv ℂ (f n)) (fderiv ℂ g) l U

Locally uniform convergence of the Fréchet derivatives, without a choice of coordinates in the statement. The target carries the operator norm.

theorem TendstoLocallyUniformlyOn.iteratedFDeriv_finiteDimensionalCarlson {κ : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} {l : Filter κ} [l.NeBot] {f : κ → E → F} {g : E → F} (hlim : TendstoLocallyUniformlyOn f g l U) (hf : ∀ᶠ (n : κ) in l, AnalyticOnNhd ℂ (f n) U) (hU : IsOpen U) (k : ℕ) : TendstoLocallyUniformlyOn (fun (n : κ) => iteratedFDeriv ℂ k (f n)) (iteratedFDeriv ℂ k g) l U

All iterated Fréchet derivatives converge locally uniformly on a finite-dimensional complex domain, in multilinear operator norm.