Swapping limits and derivatives via uniform convergence #
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 hasFDerivAt_of_tendstoLocallyUniformlyOn.
Main statements #
uniformCauchySeqOnFilter_of_fderiv: Iff : ℕ → E → Gis a sequence of functions which have derivativesf' : ℕ → E → (E →L[𝕜] G)on a neighborhood ofx,- the functions
fconverge atx, and - the derivatives
f'form a Cauchy sequence uniformly on a neighborhood ofx, then thefform a Cauchy sequence uniformly on a neighborhood ofx
hasFDerivAt_of_tendstoUniformlyOnFilter: Suppose (1), (2), and (3) above are true. Letg(resp.g') be the limiting function of thef(resp.g'). Thenf'is the derivative ofgon a neighborhood ofxhasFDerivAt_of_tendstoUniformlyOn: 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 quantifiers
∀ ε > 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 atTop, 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)|) (atTop ×ˢ 𝓝 x) (𝓝 0)
but this is equivalent to the quantifier 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)|) (atTop.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 hasFDerivAt_of_tendstoUniformlyOnFilter 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
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.
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_uniformCauchySeqOn_fderiv.
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.
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)
(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': Thef'converge "uniformly at"xtog'. This does not mean that thef' neven converge away fromx!hf: For all(y, n)withysufficiently close toxandnsufficiently large,f' nis the derivative off nhfg: Thef nconverge pointwise togon a neighborhood ofx
A slight variant of hasFDerivAt_of_tendstoLocallyUniformlyOn with the assumption stated
in terms of DifferentiableOn rather than HasFDerivAt. This makes a few proofs nicer in
complex analysis where holomorphicity is assumed but the derivative is not known a priori.
(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.
(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.
If our derivatives converge uniformly, then the Fréchet derivatives converge uniformly
A slight variant of hasDerivAt_of_tendstoLocallyUniformlyOn with the assumption stated in
terms of DifferentiableOn rather than HasDerivAt. This makes a few proofs nicer in complex
analysis where holomorphicity is assumed but the derivative is not known a priori.