mathlib documentation

analysis.complex.locally_uniform_limit

Locally uniform limits of holomorphic functions #

This file gathers some results about locally uniform limits of holomorphic functions on an open subset of the complex plane.

Main results #

noncomputable def complex.cderiv {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] (r : ) (f : E) (z : ) :
E

A circle integral which coincides with deriv f z whenever one can apply the Cauchy formula for the derivative. It is useful in the proof that locally uniform limits of holomorphic functions are holomorphic, because it depends continuously on f for the uniform topology.

Equations
theorem complex.cderiv_eq_deriv {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {U : set } {z : } {r : } {f : E} (hU : is_open U) (hf : differentiable_on f U) (hr : 0 < r) (hzr : metric.closed_ball z r U) :
theorem complex.norm_cderiv_le {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {z : } {M r : } {f : E} (hr : 0 < r) (hf : (w : ), w metric.sphere z r f w M) :
theorem complex.cderiv_sub {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {z : } {r : } {f g : E} (hr : 0 < r) (hf : continuous_on f (metric.sphere z r)) (hg : continuous_on g (metric.sphere z r)) :
theorem complex.norm_cderiv_lt {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {z : } {M r : } {f : E} (hr : 0 < r) (hfM : (w : ), w metric.sphere z r f w < M) (hf : continuous_on f (metric.sphere z r)) :
theorem complex.norm_cderiv_sub_lt {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {z : } {M r : } {f g : E} (hr : 0 < r) (hfg : (w : ), w metric.sphere z r f w - g w < M) (hf : continuous_on f (metric.sphere z r)) (hg : continuous_on g (metric.sphere z r)) :
theorem complex.tendsto_uniformly_on.cderiv {E : Type u_1} {ι : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {K : set } {δ : } {φ : filter ι} {F : ι E} {f : E} (hF : tendsto_uniformly_on F f φ (metric.cthickening δ K)) (hδ : 0 < δ) (hFn : ∀ᶠ (n : ι) in φ, continuous_on (F n) (metric.cthickening δ K)) :
theorem complex.tendsto_uniformly_on_deriv_of_cthickening_subset {E : Type u_1} {ι : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {U K : set } {φ : filter ι} {F : ι E} {f : E} (hf : tendsto_locally_uniformly_on F f φ U) (hF : ∀ᶠ (n : ι) in φ, differentiable_on (F n) U) {δ : } (hδ : 0 < δ) (hK : is_compact K) (hU : is_open U) (hKU : metric.cthickening δ K U) :
theorem complex.exists_cthickening_tendsto_uniformly_on {E : Type u_1} {ι : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {U K : set } {φ : filter ι} {F : ι E} {f : E} (hf : tendsto_locally_uniformly_on F f φ U) (hF : ∀ᶠ (n : ι) in φ, differentiable_on (F n) U) (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(δ : ) (H : δ > 0), metric.cthickening δ K U tendsto_uniformly_on (deriv F) (complex.cderiv δ f) φ K
theorem tendsto_locally_uniformly_on.differentiable_on {E : Type u_1} {ι : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {U : set } {φ : filter ι} {F : ι E} {f : E} [φ.ne_bot] (hf : tendsto_locally_uniformly_on F f φ U) (hF : ∀ᶠ (n : ι) in φ, differentiable_on (F n) U) (hU : is_open U) :

A locally uniform limit of holomorphic functions on an open domain of the complex plane is holomorphic (the derivatives converge locally uniformly to that of the limit, which is proved as tendsto_locally_uniformly_on.deriv).

theorem tendsto_locally_uniformly_on.deriv {E : Type u_1} {ι : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {U : set } {φ : filter ι} {F : ι E} {f : E} (hf : tendsto_locally_uniformly_on F f φ U) (hF : ∀ᶠ (n : ι) in φ, differentiable_on (F n) U) (hU : is_open U) :