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 : ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousWithinAt f s x

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 : ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousAt f x

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 : ∀ x ∈ s, ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousOn f s

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 : ∀ u ∈ uniformity β, ∃ (F : α → β), ContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u) : ContinuousOn f s

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 : α), ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : Continuous f

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 : ∀ u ∈ uniformity β, ∃ (F : α → β), Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u) : Continuous f

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] : ContinuousOn f s

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] : ContinuousOn f s

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] : Continuous f

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] : Continuous f

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 : ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (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 : ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (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.