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 #
TendstoLocallyUniformlyOn.differentiableOn: A locally uniform limit of holomorphic functions is holomorphic.TendstoLocallyUniformlyOn.deriv: Locally uniform convergence implies locally uniform convergence of the derivatives to the derivative of the limit.
noncomputable def
Complex.cderiv
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ 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
Instances For
theorem
Complex.cderiv_eq_deriv
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{U : Set ℂ}
{z : ℂ}
{r : ℝ}
{f : ℂ → E}
[CompleteSpace E]
(hU : IsOpen U)
(hf : DifferentiableOn ℂ f U)
(hr : 0 < r)
(hzr : Metric.closedBall z r ⊆ U)
:
Complex.cderiv r f z = deriv f z
theorem
Complex.norm_cderiv_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{z : ℂ}
{M r : ℝ}
{f : ℂ → E}
(hr : 0 < r)
(hf : ∀ w ∈ Metric.sphere z r, ‖f w‖ ≤ M)
:
‖Complex.cderiv r f z‖ ≤ M / r
theorem
Complex.cderiv_sub
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{z : ℂ}
{r : ℝ}
{f g : ℂ → E}
(hr : 0 < r)
(hf : ContinuousOn f (Metric.sphere z r))
(hg : ContinuousOn g (Metric.sphere z r))
:
Complex.cderiv r (f - g) z = Complex.cderiv r f z - Complex.cderiv r g z
theorem
Complex.norm_cderiv_lt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{z : ℂ}
{M r : ℝ}
{f : ℂ → E}
(hr : 0 < r)
(hfM : ∀ w ∈ Metric.sphere z r, ‖f w‖ < M)
(hf : ContinuousOn f (Metric.sphere z r))
:
‖Complex.cderiv r f z‖ < M / r
theorem
Complex.norm_cderiv_sub_lt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{z : ℂ}
{M r : ℝ}
{f g : ℂ → E}
(hr : 0 < r)
(hfg : ∀ w ∈ Metric.sphere z r, ‖f w - g w‖ < M)
(hf : ContinuousOn f (Metric.sphere z r))
(hg : ContinuousOn g (Metric.sphere z r))
:
‖Complex.cderiv r f z - Complex.cderiv r g z‖ < M / r
theorem
TendstoUniformlyOn.cderiv
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{K : Set ℂ}
{δ : ℝ}
{φ : Filter ι}
{F : ι → ℂ → E}
{f : ℂ → E}
(hF : TendstoUniformlyOn F f φ (Metric.cthickening δ K))
(hδ : 0 < δ)
(hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (Metric.cthickening δ K))
:
TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
theorem
Complex.tendstoUniformlyOn_deriv_of_cthickening_subset
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{U K : Set ℂ}
{φ : Filter ι}
{F : ι → ℂ → E}
{f : ℂ → E}
[CompleteSpace E]
(hf : TendstoLocallyUniformlyOn F f φ U)
(hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U)
{δ : ℝ}
(hδ : 0 < δ)
(hK : IsCompact K)
(hU : IsOpen U)
(hKU : Metric.cthickening δ K ⊆ U)
:
TendstoUniformlyOn (deriv ∘ F) (Complex.cderiv δ f) φ K
theorem
Complex.exists_cthickening_tendstoUniformlyOn
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{U K : Set ℂ}
{φ : Filter ι}
{F : ι → ℂ → E}
{f : ℂ → E}
[CompleteSpace E]
(hf : TendstoLocallyUniformlyOn F f φ U)
(hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U)
(hK : IsCompact K)
(hU : IsOpen U)
(hKU : K ⊆ U)
:
∃ δ > 0, Metric.cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (Complex.cderiv δ f) φ K
theorem
TendstoLocallyUniformlyOn.differentiableOn
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{U : Set ℂ}
{φ : Filter ι}
{F : ι → ℂ → E}
{f : ℂ → E}
[CompleteSpace E]
[φ.NeBot]
(hf : TendstoLocallyUniformlyOn F f φ U)
(hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U)
(hU : IsOpen U)
:
DifferentiableOn ℂ f 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 TendstoLocallyUniformlyOn.deriv).
theorem
TendstoLocallyUniformlyOn.deriv
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{U : Set ℂ}
{φ : Filter ι}
{F : ι → ℂ → E}
{f : ℂ → E}
[CompleteSpace E]
(hf : TendstoLocallyUniformlyOn F f φ U)
(hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U)
(hU : IsOpen U)
:
TendstoLocallyUniformlyOn (deriv ∘ F) (deriv f) φ U
theorem
Complex.differentiableOn_tsum_of_summable_norm
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{U : Set ℂ}
{F : ι → ℂ → E}
[CompleteSpace E]
{u : ι → ℝ}
(hu : Summable u)
(hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U)
(hU : IsOpen U)
(hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i)
:
DifferentiableOn ℂ (fun (w : ℂ) => ∑' (i : ι), F i w) U
If the terms in the sum ∑' (i : ι), F i are uniformly bounded on U by a
summable function, and each term in the sum is differentiable on U, then so is the sum.
theorem
Complex.hasSum_deriv_of_summable_norm
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{U : Set ℂ}
{z : ℂ}
{F : ι → ℂ → E}
[CompleteSpace E]
{u : ι → ℝ}
(hu : Summable u)
(hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U)
(hU : IsOpen U)
(hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i)
(hz : z ∈ U)
:
If the terms in the sum ∑' (i : ι), F i are uniformly bounded on U by a
summable function, then the sum of deriv F i at a point in U is the derivative of the
sum.
theorem
Complex.logDeriv_tendsto
{ι : Type u_3}
{p : Filter ι}
(f : ι → ℂ → ℂ)
(g : ℂ → ℂ)
{s : Set ℂ}
(hs : IsOpen s)
(x : ↑s)
(hF : TendstoLocallyUniformlyOn f g p s)
(hf : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (f n) s)
(hg : g ↑x ≠ 0)
:
Filter.Tendsto (fun (n : ι) => logDeriv (f n) ↑x) p (nhds (logDeriv g ↑x))
The logarithmic derivative of a sequence of functions converging locally uniformly to a function is the logarithmic derivative of the limit function.