Uniform convergence #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A sequence of functions Fₙ (with values in a metric space) converges uniformly on a set s to a
function f if, for all ε > 0, for all large enough n, one has for all y ∈ s the inequality
dist (f y, Fₙ y) < ε. Under uniform convergence, many properties of the Fₙ pass to the limit,
most notably continuity. We prove this in the file, defining the notion of uniform convergence
in the more general setting of uniform spaces, and with respect to an arbitrary indexing set
endowed with a filter (instead of just ℕ with at_top).
Main results #
Let α be a topological space, β a uniform space, Fₙ and f be functions from αto β
(where the index n belongs to an indexing type ι endowed with a filter p).
tendsto_uniformly_on F f p s: the fact thatFₙconverges uniformly tofons. This means that, for any entourageuof the diagonal, for large enoughn(with respect top), one has(f y, Fₙ y) ∈ ufor ally ∈ s.tendsto_uniformly F f p: same notion withs = univ.tendsto_uniformly_on.continuous_on: a uniform limit on a set of functions which are continuous on this set is itself continuous on this set.tendsto_uniformly.continuous: a uniform limit of continuous functions is continuous.tendsto_uniformly_on.tendsto_comp: IfFₙtends uniformly tofon a sets, andgₙtends toxwithins, thenFₙ gₙtends tof xiffis continuous atxwithins.tendsto_uniformly.tendsto_comp: IfFₙtends uniformly tof, andgₙtends tox, thenFₙ gₙtends tof x.
We also define notions where the convergence is locally uniform, called
tendsto_locally_uniformly_on F f p s and tendsto_locally_uniformly F f p. The previous theorems
all have corresponding versions under locally uniform convergence.
Finally, we introduce the notion of a uniform Cauchy sequence, which is to uniform convergence what a Cauchy sequence is to the usual notion of convergence.
Implementation notes #
We derive most of our initial results from an auxiliary definition tendsto_uniformly_on_filter.
This definition in and of itself can sometimes be useful, e.g., when studying the local behavior
of the Fₙ near a point, which would typically look like tendsto_uniformly_on_filter F f p (𝓝 x).
Still, while this may be the "correct" definition (see
tendsto_uniformly_on_iff_tendsto_uniformly_on_filter), it is somewhat unwieldy to work with in
practice. Thus, we provide the more traditional definition in tendsto_uniformly_on.
Most results hold under weaker assumptions of locally uniform approximation. In a first section, we prove the results under these weaker assumptions. Then, we derive the results on uniform convergence from them.
Tags #
Uniform limit, uniform convergence, tends uniformly to
Different notions of uniform convergence #
We define uniform convergence and locally uniform convergence, on a set or in the whole space.
A sequence of functions Fₙ converges uniformly on a filter p' to a limiting function f
with respect to the filter p if, for any entourage of the diagonal u, one has
p ×ᶠ p'-eventually (f x, Fₙ x) ∈ u.
A sequence of functions Fₙ converges uniformly on a filter p' to a limiting function f w.r.t.
filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ᶠ p' to the uniformity.
In other words: one knows nothing about the behavior of x in this limit besides it being in p'.
A sequence of functions Fₙ converges uniformly on a set s to a limiting function f with
respect to the filter p if, for any entourage of the diagonal u, one has p-eventually
(f x, Fₙ x) ∈ u for all x ∈ s.
Alias of the reverse direction of tendsto_uniformly_on_iff_tendsto_uniformly_on_filter.
Alias of the forward direction of tendsto_uniformly_on_iff_tendsto_uniformly_on_filter.
A sequence of functions Fₙ converges uniformly on a set s to a limiting function f w.r.t.
filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ᶠ 𝓟 s to the uniformity.
In other words: one knows nothing about the behavior of x in this limit besides it being in s.
A sequence of functions Fₙ converges uniformly to a limiting function f with respect to a
filter p if, for any entourage of the diagonal u, one has p-eventually
(f x, Fₙ x) ∈ u for all x.
A sequence of functions Fₙ converges uniformly to a limiting function f w.r.t.
filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ᶠ ⊤ to the uniformity.
In other words: one knows nothing about the behavior of x in this limit.
Uniform converence implies pointwise convergence.
Uniform converence implies pointwise convergence.
Uniform converence implies pointwise convergence.
Composing on the right by a function preserves uniform convergence on a filter
Composing on the right by a function preserves uniform convergence on a set
Composing on the right by a function preserves uniform convergence
Composing on the left by a uniformly continuous function preserves uniform convergence on a filter
Composing on the left by a uniformly continuous function preserves uniform convergence on a set
Composing on the left by a uniformly continuous function preserves uniform convergence
Uniform convergence on a filter p' to a constant function is equivalent to convergence in
p ×ᶠ p'.
Uniform convergence on a set s to a constant function is equivalent to convergence in
p ×ᶠ 𝓟 s.
Uniform convergence to a constant function is equivalent to convergence in p ×ᶠ ⊤.
Uniform convergence on the empty set is vacuously true
Uniform convergence on a singleton is equivalent to regular convergence
If a sequence g converges to some b, then the sequence of constant functions
λ n, λ a, g n converges to the constant function λ a, b on any set s
If a sequence g converges to some b, then the sequence of constant functions
λ n, λ a, g n converges to the constant function λ a, b on any set s
A sequence is uniformly Cauchy if eventually all of its pairwise differences are uniformly bounded
A sequence is uniformly Cauchy if eventually all of its pairwise differences are uniformly bounded
A sequence that converges uniformly is also uniformly Cauchy
A sequence that converges uniformly is also uniformly Cauchy
A uniformly Cauchy sequence converges uniformly to its limit
A uniformly Cauchy sequence converges uniformly to its limit
Composing on the right by a function preserves uniform Cauchy sequences
Composing on the right by a function preserves uniform Cauchy sequences
Composing on the left by a uniformly continuous function preserves uniform Cauchy sequences
If a sequence of functions is uniformly Cauchy on a set, then the values at each point form a Cauchy sequence.
A sequence of functions Fₙ converges locally uniformly on a set s to a limiting function
f with respect to a filter p if, for any entourage of the diagonal u, for any x ∈ s, one
has p-eventually (f y, Fₙ y) ∈ u for all y in a neighborhood of x in s.
A sequence of functions Fₙ converges locally uniformly to a limiting function f with respect
to a filter p if, for any entourage of the diagonal u, for any x, one has p-eventually
(f y, Fₙ y) ∈ u for all y in a neighborhood of x.
On a compact space, locally uniform convergence is just uniform convergence.
For a compact set s, locally uniform convergence on s is just uniform convergence on s.
Uniform approximation #
In this section, we give lemmas ensuring that a function is continuous if it can be approximated
uniformly by continuous functions. We give various versions, within a set or the whole space, at
a single point or at all points, with locally uniform approximation or uniform approximation. All
the statements are derived from a statement about locally uniform approximation within a set at
a point, called continuous_within_at_of_locally_uniform_approx_of_continuous_within_at.
A function which can be locally uniformly approximated by functions which are continuous within a set at a point is continuous within this set at this point.
A function which can be locally uniformly approximated by functions which are continuous at a point is continuous at this point.
A function which can be locally uniformly approximated by functions which are continuous on a set is continuous on this set.
A function which can be uniformly approximated by functions which are continuous on a set is continuous on this set.
A function which can be locally uniformly approximated by continuous functions is continuous.
A function which can be uniformly approximated by continuous functions is continuous.
Uniform limits #
From the previous statements on uniform approximation, we deduce continuity results for uniform limits.
A locally uniform limit on a set of functions which are continuous on this set is itself continuous on this set.
A uniform limit on a set of functions which are continuous on this set is itself continuous on this set.
A locally uniform limit of continuous functions is continuous.
A uniform limit of continuous functions is continuous.
Composing limits under uniform convergence #
In general, if Fₙ converges pointwise to a function f, and gₙ tends to x, it is not true
that Fₙ gₙ tends to f x. It is true however if the convergence of Fₙ to f is uniform. In
this paragraph, we prove variations around this statement.
If Fₙ converges locally uniformly on a neighborhood of x within a set s to a function f
which is continuous at x within s, and gₙ tends to x within s, then Fₙ (gₙ) tends
to f x.
If Fₙ converges locally uniformly on a neighborhood of x to a function f which is
continuous at x, and gₙ tends to x, then Fₙ (gₙ) tends to f x.
If Fₙ tends locally uniformly to f on a set s, and gₙ tends to x within s, then
Fₙ gₙ tends to f x if f is continuous at x within s and x ∈ s.
If Fₙ tends uniformly to f on a set s, and gₙ tends to x within s, then Fₙ gₙ
tends to f x if f is continuous at x within s.
If Fₙ tends locally uniformly to f, and gₙ tends to x, then Fₙ gₙ tends to f x.
If Fₙ tends uniformly to f, and gₙ tends to x, then Fₙ gₙ tends to f x.