mathlib3 documentation

analysis.calculus.uniform_limits_deriv

Swapping limits and derivatives via uniform convergence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The purpose of this file is to prove that the derivative of the pointwise limit of a sequence of functions is the pointwise limit of the functions' derivatives when the derivatives converge uniformly. The formal statement appears as has_fderiv_at_of_tendsto_locally_uniformly_at.

Main statements #

Each of the above statements also has variations that support deriv instead of fderiv.

Implementation notes #

Our technique for proving the main result is the famous "ε / 3 proof." In words, you can find it explained, for instance, at this StackExchange post. The subtlety is that we want to prove that the difference quotients of the g converge to the g'. That is, we want to prove something like:

 ε > 0,  δ > 0,  y  B_δ(x), |y - x|⁻¹ * |(g y - g x) - g' x (y - x)| < ε.

To do so, we will need to introduce a pair of quantifers

 ε > 0,  N,  n  N,  δ > 0,  y  B_δ(x), |y - x|⁻¹ * |(g y - g x) - g' x (y - x)| < ε.

So how do we write this in terms of filters? Well, the initial definition of the derivative is

tendsto (|y - x|⁻¹ * |(g y - g x) - g' x (y - x)|) (𝓝 x) (𝓝 0)

There are two ways we might introduce n. We could do:

∀ᶠ (n : ) in at_top, tendsto (|y - x|⁻¹ * |(g y - g x) - g' x (y - x)|) (𝓝 x) (𝓝 0)

but this is equivalent to the quantifier order ∃ N, ∀ n ≥ N, ∀ ε > 0, ∃ δ > 0, ∀ y ∈ B_δ(x), which implies our desired ∀ ∃ ∀ ∃ ∀ but is not equivalent to it. On the other hand, we might try

tendsto (|y - x|⁻¹ * |(g y - g x) - g' x (y - x)|) (at_top ×ᶠ 𝓝 x) (𝓝 0)

but this is equivalent to the quantifer order ∀ ε > 0, ∃ N, ∃ δ > 0, ∀ n ≥ N, ∀ y ∈ B_δ(x), which again implies our desired ∀ ∃ ∀ ∃ ∀ but is not equivalent to it.

So to get the quantifier order we want, we need to introduce a new filter construction, which we call a "curried filter"

tendsto (|y - x|⁻¹ * |(g y - g x) - g' x (y - x)|) (at_top.curry (𝓝 x)) (𝓝 0)

Then the above implications are filter.tendsto.curry and filter.tendsto.mono_left filter.curry_le_prod. We will use both of these deductions as part of our proof.

We note that if you loosen the assumptions of the main theorem then the proof becomes quite a bit easier. In particular, if you assume there is a common neighborhood s where all of the three assumptions of has_fderiv_at_of_tendsto_uniformly_on_filter hold and that the f' are continuous, then you can avoid the mean value theorem and much of the work around curried filters.

Tags #

uniform convergence, limits of derivatives

theorem uniform_cauchy_seq_on_filter_of_fderiv {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {f' : ι E (E →L[𝕜] G)} {x : E} (hf' : uniform_cauchy_seq_on_filter f' l (nhds x)) (hf : ∀ᶠ (n : ι × E) in l.prod (nhds x), has_fderiv_at (f n.fst) (f' n.fst n.snd) n.snd) (hfg : cauchy (filter.map (λ (n : ι), f n x) l)) :

If a sequence of functions real or complex functions are eventually differentiable on a neighborhood of x, they are Cauchy at x, and their derivatives are a uniform Cauchy sequence in a neighborhood of x, then the functions form a uniform Cauchy sequence in a neighborhood of x.

theorem uniform_cauchy_seq_on_ball_of_fderiv {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {f' : ι E (E →L[𝕜] G)} {x : E} {r : } (hf' : uniform_cauchy_seq_on f' l (metric.ball x r)) (hf : (n : ι) (y : E), y metric.ball x r has_fderiv_at (f n) (f' n y) y) (hfg : cauchy (filter.map (λ (n : ι), f n x) l)) :

A variant of the second fundamental theorem of calculus (FTC-2): If a sequence of functions between real or complex normed spaces are differentiable on a ball centered at x, they form a Cauchy sequence at x, and their derivatives are Cauchy uniformly on the ball, then the functions form a uniform Cauchy sequence on the ball.

NOTE: The fact that we work on a ball is typically all that is necessary to work with power series and Dirichlet series (our primary use case). However, this can be generalized by replacing the ball with any connected, bounded, open set and replacing uniform convergence with local uniform convergence. See cauchy_map_of_uniform_cauchy_seq_on_fderiv.

theorem cauchy_map_of_uniform_cauchy_seq_on_fderiv {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {f' : ι E (E →L[𝕜] G)} {s : set E} (hs : is_open s) (h's : is_preconnected s) (hf' : uniform_cauchy_seq_on f' l s) (hf : (n : ι) (y : E), y s has_fderiv_at (f n) (f' n y) y) {x₀ x : E} (hx₀ : x₀ s) (hx : x s) (hfg : cauchy (filter.map (λ (n : ι), f n x₀) l)) :
cauchy (filter.map (λ (n : ι), f n x) l)

If a sequence of functions between real or complex normed spaces are differentiable on a preconnected open set, they form a Cauchy sequence at x, and their derivatives are Cauchy uniformly on the set, then the functions form a Cauchy sequence at any point in the set.

theorem difference_quotients_converge_uniformly {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {g : E G} {f' : ι E (E →L[𝕜] G)} {g' : E (E →L[𝕜] G)} {x : E} (hf' : tendsto_uniformly_on_filter f' g' l (nhds x)) (hf : ∀ᶠ (n : ι × E) in l.prod (nhds x), has_fderiv_at (f n.fst) (f' n.fst n.snd) n.snd) (hfg : ∀ᶠ (y : E) in nhds x, filter.tendsto (λ (n : ι), f n y) l (nhds (g y))) :
tendsto_uniformly_on_filter (λ (n : ι) (y : E), (y - x)⁻¹ (f n y - f n x)) (λ (y : E), (y - x)⁻¹ (g y - g x)) l (nhds x)

If f_n → g pointwise and the derivatives (f_n)' → h uniformly converge, then in fact for a fixed y, the difference quotients ‖z - y‖⁻¹ • (f_n z - f_n y) converge uniformly to ‖z - y‖⁻¹ • (g z - g y)

theorem has_fderiv_at_of_tendsto_uniformly_on_filter {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {g : E G} {f' : ι E (E →L[𝕜] G)} {g' : E (E →L[𝕜] G)} {x : E} [l.ne_bot] (hf' : tendsto_uniformly_on_filter f' g' l (nhds x)) (hf : ∀ᶠ (n : ι × E) in l.prod (nhds x), has_fderiv_at (f n.fst) (f' n.fst n.snd) n.snd) (hfg : ∀ᶠ (y : E) in nhds x, filter.tendsto (λ (n : ι), f n y) l (nhds (g y))) :
has_fderiv_at g (g' x) x

(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x when the f' n converge uniformly to their limit at x.

In words the assumptions mean the following:

  • hf': The f' converge "uniformly at" x to g'. This does not mean that the f' n even converge away from x!
  • hf: For all (y, n) with y sufficiently close to x and n sufficiently large, f' n is the derivative of f n
  • hfg: The f n converge pointwise to g on a neighborhood of x
theorem has_fderiv_at_of_tendsto_locally_uniformly_on {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {g : E G} {f' : ι E (E →L[𝕜] G)} {g' : E (E →L[𝕜] G)} {x : E} [l.ne_bot] {s : set E} (hs : is_open s) (hf' : tendsto_locally_uniformly_on f' g' l s) (hf : (n : ι) (x : E), x s has_fderiv_at (f n) (f' n x) x) (hfg : (x : E), x s filter.tendsto (λ (n : ι), f n x) l (nhds (g x))) (hx : x s) :
has_fderiv_at g (g' x) x
theorem has_fderiv_at_of_tendsto_locally_uniformly_on' {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {g : E G} {g' : E (E →L[𝕜] G)} {x : E} [l.ne_bot] {s : set E} (hs : is_open s) (hf' : tendsto_locally_uniformly_on (fderiv 𝕜 f) g' l s) (hf : (n : ι), differentiable_on 𝕜 (f n) s) (hfg : (x : E), x s filter.tendsto (λ (n : ι), f n x) l (nhds (g x))) (hx : x s) :
has_fderiv_at g (g' x) x

A slight variant of has_fderiv_at_of_tendsto_locally_uniformly_on with the assumption stated in terms of differentiable_on rather than has_fderiv_at. This makes a few proofs nicer in complex analysis where holomorphicity is assumed but the derivative is not known a priori.

theorem has_fderiv_at_of_tendsto_uniformly_on {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {g : E G} {f' : ι E (E →L[𝕜] G)} {g' : E (E →L[𝕜] G)} [l.ne_bot] {s : set E} (hs : is_open s) (hf' : tendsto_uniformly_on f' g' l s) (hf : (n : ι) (x : E), x s has_fderiv_at (f n) (f' n x) x) (hfg : (x : E), x s filter.tendsto (λ (n : ι), f n x) l (nhds (g x))) (x : E) :
x s has_fderiv_at g (g' x) x

(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x when the f' n converge uniformly to their limit on an open set containing x.

theorem has_fderiv_at_of_tendsto_uniformly {ι : Type u_1} {l : filter ι} {E : Type u_2} [normed_add_comm_group E] {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_space 𝕜 E] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι E G} {g : E G} {f' : ι E (E →L[𝕜] G)} {g' : E (E →L[𝕜] G)} [l.ne_bot] (hf' : tendsto_uniformly f' g' l) (hf : (n : ι) (x : E), has_fderiv_at (f n) (f' n x) x) (hfg : (x : E), filter.tendsto (λ (n : ι), f n x) l (nhds (g x))) (x : E) :
has_fderiv_at g (g' x) x

(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x when the f' n converge uniformly to their limit.

deriv versions of above theorems #

In this section, we provide deriv equivalents of the fderiv lemmas in the previous section. The protected function promote_deriv provides the translation between derivatives and Fréchet derivatives

theorem uniform_cauchy_seq_on_filter.one_smul_right {ι : Type u_1} {l : filter ι} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : Type u_3} [normed_add_comm_group G] [normed_space 𝕜 G] {f' : ι 𝕜 G} {l' : filter 𝕜} (hf' : uniform_cauchy_seq_on_filter f' l l') :
uniform_cauchy_seq_on_filter (λ (n : ι) (z : 𝕜), 1.smul_right (f' n z)) l l'

If our derivatives converge uniformly, then the Fréchet derivatives converge uniformly

theorem uniform_cauchy_seq_on_filter_of_deriv {ι : Type u_1} {l : filter ι} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : Type u_3} [normed_add_comm_group G] [normed_space 𝕜 G] {f f' : ι 𝕜 G} {x : 𝕜} (hf' : uniform_cauchy_seq_on_filter f' l (nhds x)) (hf : ∀ᶠ (n : ι × 𝕜) in l.prod (nhds x), has_deriv_at (f n.fst) (f' n.fst n.snd) n.snd) (hfg : cauchy (filter.map (λ (n : ι), f n x) l)) :
theorem uniform_cauchy_seq_on_ball_of_deriv {ι : Type u_1} {l : filter ι} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : Type u_3} [normed_add_comm_group G] [normed_space 𝕜 G] {f f' : ι 𝕜 G} {x : 𝕜} {r : } (hf' : uniform_cauchy_seq_on f' l (metric.ball x r)) (hf : (n : ι) (y : 𝕜), y metric.ball x r has_deriv_at (f n) (f' n y) y) (hfg : cauchy (filter.map (λ (n : ι), f n x) l)) :
theorem has_deriv_at_of_tendsto_uniformly_on_filter {ι : Type u_1} {l : filter ι} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : Type u_3} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι 𝕜 G} {g : 𝕜 G} {f' : ι 𝕜 G} {g' : 𝕜 G} {x : 𝕜} [l.ne_bot] (hf' : tendsto_uniformly_on_filter f' g' l (nhds x)) (hf : ∀ᶠ (n : ι × 𝕜) in l.prod (nhds x), has_deriv_at (f n.fst) (f' n.fst n.snd) n.snd) (hfg : ∀ᶠ (y : 𝕜) in nhds x, filter.tendsto (λ (n : ι), f n y) l (nhds (g y))) :
has_deriv_at g (g' x) x
theorem has_deriv_at_of_tendsto_locally_uniformly_on {ι : Type u_1} {l : filter ι} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : Type u_3} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι 𝕜 G} {g : 𝕜 G} {f' : ι 𝕜 G} {g' : 𝕜 G} {x : 𝕜} [l.ne_bot] {s : set 𝕜} (hs : is_open s) (hf' : tendsto_locally_uniformly_on f' g' l s) (hf : ∀ᶠ (n : ι) in l, (x : 𝕜), x s has_deriv_at (f n) (f' n x) x) (hfg : (x : 𝕜), x s filter.tendsto (λ (n : ι), f n x) l (nhds (g x))) (hx : x s) :
has_deriv_at g (g' x) x
theorem has_deriv_at_of_tendsto_locally_uniformly_on' {ι : Type u_1} {l : filter ι} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : Type u_3} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι 𝕜 G} {g g' : 𝕜 G} {x : 𝕜} [l.ne_bot] {s : set 𝕜} (hs : is_open s) (hf' : tendsto_locally_uniformly_on (deriv f) g' l s) (hf : ∀ᶠ (n : ι) in l, differentiable_on 𝕜 (f n) s) (hfg : (x : 𝕜), x s filter.tendsto (λ (n : ι), f n x) l (nhds (g x))) (hx : x s) :
has_deriv_at g (g' x) x

A slight variant of has_deriv_at_of_tendsto_locally_uniformly_on with the assumption stated in terms of differentiable_on rather than has_deriv_at. This makes a few proofs nicer in complex analysis where holomorphicity is assumed but the derivative is not known a priori.

theorem has_deriv_at_of_tendsto_uniformly_on {ι : Type u_1} {l : filter ι} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : Type u_3} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι 𝕜 G} {g : 𝕜 G} {f' : ι 𝕜 G} {g' : 𝕜 G} [l.ne_bot] {s : set 𝕜} (hs : is_open s) (hf' : tendsto_uniformly_on f' g' l s) (hf : ∀ᶠ (n : ι) in l, (x : 𝕜), x s has_deriv_at (f n) (f' n x) x) (hfg : (x : 𝕜), x s filter.tendsto (λ (n : ι), f n x) l (nhds (g x))) (x : 𝕜) :
x s has_deriv_at g (g' x) x
theorem has_deriv_at_of_tendsto_uniformly {ι : Type u_1} {l : filter ι} {𝕜 : Type u_2} [is_R_or_C 𝕜] {G : Type u_3} [normed_add_comm_group G] [normed_space 𝕜 G] {f : ι 𝕜 G} {g : 𝕜 G} {f' : ι 𝕜 G} {g' : 𝕜 G} [l.ne_bot] (hf' : tendsto_uniformly f' g' l) (hf : ∀ᶠ (n : ι) in l, (x : 𝕜), has_deriv_at (f n) (f' n x) x) (hfg : (x : 𝕜), filter.tendsto (λ (n : ι), f n x) l (nhds (g x))) (x : 𝕜) :
has_deriv_at g (g' x) x