Uniform limits of holomorphic maps on a complex normed space

Mathlib's TendstoLocallyUniformlyOn.differentiableOn shows that a locally uniform limit of holomorphic functions on an open subset of ℂ is holomorphic; its proof uses the Cauchy integral formula on circles. This file proves the corresponding statement for uniform limits on an open subset of an arbitrary complex normed space V, with values in a complex Banach space E (TendstoUniformlyOn.differentiableOn). It is the input needed to see that bounded holomorphic functions form a closed subspace of the bounded continuous functions.

Main results

• TauCeti.norm_fderiv_le_of_forall_mem_ball_norm_le: if ‖f‖ ≤ M on ball c r, then ‖fderiv ℂ f c‖ ≤ 2 * M / r.
• TendstoUniformlyOn.differentiableOn: a uniform limit of holomorphic maps on an open set is holomorphic.

References

• J. Mujica, Complex Analysis in Banach Spaces, North-Holland Mathematics Studies 120, North-Holland, 1986.

theorem TauCeti.norm_fderiv_le_of_forall_mem_ball_norm_le {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} {c : V} {r M : ℝ} (hd : DifferentiableOn ℂ f (Metric.ball c r)) (hr : 0 < r) (hM : ∀ y ∈ Metric.ball c r, ‖f y‖ ≤ M) : ‖fderiv ℂ f c‖ ≤ 2 * M / r

Cauchy's estimate on a ball in a complex normed space. If f is holomorphic on ball c r and bounded there by M, then ‖fderiv ℂ f c‖ ≤ 2 * M / r.

theorem TendstoUniformlyOn.differentiableOn {V : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {l : Filter ι} [l.NeBot] {F : ι → V → E} {f : V → E} {U : Set V} (hf : TendstoUniformlyOn F f l U) (hF : ∀ᶠ (n : ι) in l, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) : DifferentiableOn ℂ f U

A uniform limit of holomorphic maps is holomorphic. If holomorphic maps F n on an open subset U of a complex normed space converge uniformly on U to f, with values in a complex Banach space, then f is holomorphic on U.

This is the analogue, for domains in an arbitrary complex normed space, of Mathlib's TendstoLocallyUniformlyOn.differentiableOn for domains in ℂ.