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 #

• uniform_cauchy_seq_on_filter_of_fderiv: If
  1. f : ℕ → E → G is a sequence of functions which have derivatives f' : ℕ → E → (E →L[𝕜] G) on a neighborhood of x,
  2. the functions f converge at x, and
  3. the derivatives f' form a Cauchy sequence uniformly on a neighborhood of x, then the f form a Cauchy sequence uniformly on a neighborhood of x
• has_fderiv_at_of_tendsto_uniformly_on_filter : Suppose (1), (2), and (3) above are true. Let g (resp. g') be the limiting function of the f (resp. g'). Then f' is the derivative of g on a neighborhood of x
• has_fderiv_at_of_tendsto_uniformly_on: An often-easier-to-use version of the above theorem when all the derivatives exist and functions converge on a common open set and the derivatives converge uniformly there.

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

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