Documentation

Mathlib.Topology.UniformSpace.UniformApproximation

Uniform approximation #

In this file, 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 continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt.

Implementation notes #

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

theorem continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : αβ} {s : Set α} {x : α} (hx : x s) (L : uuniformity β, tnhdsWithin x s, ∃ (F : αβ), ContinuousWithinAt F s x yt, (f y, F y) u) :

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.

theorem continuousAt_of_locally_uniform_approx_of_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : αβ} {x : α} (L : uuniformity β, tnhds x, ∃ (F : αβ), ContinuousAt F x yt, (f y, F y) u) :

A function which can be locally uniformly approximated by functions which are continuous at a point is continuous at this point.

theorem continuousOn_of_locally_uniform_approx_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : αβ} {s : Set α} (L : xs, uuniformity β, tnhdsWithin x s, ∃ (F : αβ), ContinuousWithinAt F s x yt, (f y, F y) u) :

A function which can be locally uniformly approximated by functions which are continuous on a set is continuous on this set.

theorem continuousOn_of_uniform_approx_of_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : αβ} {s : Set α} (L : uuniformity β, ∃ (F : αβ), ContinuousOn F s ys, (f y, F y) u) :

A function which can be uniformly approximated by functions which are continuous on a set is continuous on this set.

theorem continuous_of_locally_uniform_approx_of_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : αβ} (L : ∀ (x : α), uuniformity β, tnhds x, ∃ (F : αβ), ContinuousAt F x yt, (f y, F y) u) :

A function which can be locally uniformly approximated by continuous functions is continuous.

theorem continuous_of_uniform_approx_of_continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : αβ} (L : uuniformity β, ∃ (F : αβ), Continuous F ∀ (y : α), (f y, F y) u) :

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.

theorem TendstoLocallyUniformlyOn.continuousOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {s : Set α} {p : Filter ι} (h : TendstoLocallyUniformlyOn F f p s) (hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s) [p.NeBot] :

A locally uniform limit on a set of functions which are continuous on this set is itself continuous on this set.

theorem TendstoUniformlyOn.continuousOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {s : Set α} {p : Filter ι} (h : TendstoUniformlyOn F f p s) (hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s) [p.NeBot] :

A uniform limit on a set of functions which are continuous on this set is itself continuous on this set.

theorem TendstoLocallyUniformly.continuous {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {p : Filter ι} (h : TendstoLocallyUniformly F f p) (hc : ∀ᶠ (n : ι) in p, Continuous (F n)) [p.NeBot] :

A locally uniform limit of continuous functions is continuous.

theorem TendstoUniformly.continuous {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {p : Filter ι} (h : TendstoUniformly F f p) (hc : ∀ᶠ (n : ι) in p, Continuous (F n)) [p.NeBot] :

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.

theorem tendsto_comp_of_locally_uniform_limit_within {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {s : Set α} {x : α} {p : Filter ι} {g : ια} (h : ContinuousWithinAt f s x) (hg : Filter.Tendsto g p (nhdsWithin x s)) (hunif : uuniformity β, tnhdsWithin x s, ∀ᶠ (n : ι) in p, yt, (f y, F n y) u) :
Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

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.

theorem tendsto_comp_of_locally_uniform_limit {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {x : α} {p : Filter ι} {g : ια} (h : ContinuousAt f x) (hg : Filter.Tendsto g p (nhds x)) (hunif : uuniformity β, tnhds x, ∀ᶠ (n : ι) in p, yt, (f y, F n y) u) :
Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (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.

theorem TendstoLocallyUniformlyOn.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {s : Set α} {x : α} {p : Filter ι} {g : ια} (h : TendstoLocallyUniformlyOn F f p s) (hf : ContinuousWithinAt f s x) (hx : x s) (hg : Filter.Tendsto g p (nhdsWithin x s)) :
Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (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.

theorem TendstoUniformlyOn.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {s : Set α} {x : α} {p : Filter ι} {g : ια} (h : TendstoUniformlyOn F f p s) (hf : ContinuousWithinAt f s x) (hg : Filter.Tendsto g p (nhdsWithin x s)) :
Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

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.

theorem TendstoLocallyUniformly.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {x : α} {p : Filter ι} {g : ια} (h : TendstoLocallyUniformly F f p) (hf : ContinuousAt f x) (hg : Filter.Tendsto g p (nhds x)) :
Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

If Fₙ tends locally uniformly to f, and gₙ tends to x, then Fₙ gₙ tends to f x.

theorem TendstoUniformly.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ιαβ} {f : αβ} {x : α} {p : Filter ι} {g : ια} (h : TendstoUniformly F f p) (hf : ContinuousAt f x) (hg : Filter.Tendsto g p (nhds x)) :
Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

If Fₙ tends uniformly to f, and gₙ tends to x, then Fₙ gₙ tends to f x.