Mathlib.Topology.UniformSpace.UniformApproximation

Module docstring

{"# 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 ","### Uniform limits

From the previous statements on uniform approximation, we deduce continuity results for uniform limits. ","### 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. "}

continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt theorem

 (hx : x ∈ s) (L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F : α → β, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) :
  ContinuousWithinAt f s x

Full source

/-- 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 continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (hx : x ∈ s)
    (L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F : α → β, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) :
    ContinuousWithinAt f s x := by
  refine Uniform.continuousWithinAt_iff'_left.2 fun u₀ hu₀ => ?_
  obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
  obtain ⟨u₂, h₂, hsymm, u₂₁⟩ : ∃ u ∈ 𝓤 β, (∀ {a b}, (a, b) ∈ u → (b, a) ∈ u) ∧ u ○ u ⊆ u₁ :=
    comp_symm_of_uniformity h₁
  rcases L u₂ h₂ with ⟨t, tx, F, hFc, hF⟩
  have A : ∀ᶠ y in 𝓝[s] x, (f y, F y) ∈ u₂ := Eventually.mono tx hF
  have B : ∀ᶠ y in 𝓝[s] x, (F y, F x) ∈ u₂ := Uniform.continuousWithinAt_iff'_left.1 hFc h₂
  have C : ∀ᶠ y in 𝓝[s] x, (f y, F x) ∈ u₁ :=
    (A.and B).mono fun y hy => u₂₁ (prodMk_mem_compRel hy.1 hy.2)
  have : (F x, f x)(F x, f x) ∈ u₁ :=
    u₂₁ (prodMk_mem_compRel (refl_mem_uniformity h₂) (hsymm (A.self_of_nhdsWithin hx)))
  exact C.mono fun y hy => u₁₀ (prodMk_mem_compRel hy this)

Continuity via Local Uniform Approximation within a Set at a Point

Informal description

Let $X$ be a topological space, $Y$ a uniform space, $s \subseteq X$, and $x \in s$. Suppose that for every entourage $u \in \mathfrak{U}(Y)$, there exists a neighborhood $t$ of $x$ within $s$ and a function $F \colon X \to Y$ such that: 1. $F$ is continuous at $x$ within $s$, and 2. For all $y \in t$, the pair $(f(y), F(y))$ belongs to $u$. Then $f$ is continuous at $x$ within $s$.

continuousAt_of_locally_uniform_approx_of_continuousAt theorem

(L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousAt f x

Full source

/-- A function which can be locally uniformly approximated by functions which are continuous at
a point is continuous at this point. -/
theorem continuousAt_of_locally_uniform_approx_of_continuousAt
    (L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) :
    ContinuousAt f x := by
  rw [← continuousWithinAt_univ]
  apply continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (mem_univ _) _
  simpa only [exists_prop, nhdsWithin_univ, continuousWithinAt_univ] using L

Continuity via Local Uniform Approximation at a Point

Informal description

Let $X$ be a topological space, $Y$ a uniform space, and $f \colon X \to Y$ a function. Suppose that for every entourage $u \in \mathfrak{U}(Y)$, there exists a neighborhood $t$ of $x$ in $X$ and a function $F \colon X \to Y$ such that: 1. $F$ is continuous at $x$, and 2. For all $y \in t$, the pair $(f(y), F(y))$ belongs to $u$. Then $f$ is continuous at $x$.

continuousOn_of_locally_uniform_approx_of_continuousWithinAt theorem

 (L : ∀ x ∈ s, ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousOn f s

Full source

/-- A function which can be locally uniformly approximated by functions which are continuous
on a set is continuous on this set. -/
theorem continuousOn_of_locally_uniform_approx_of_continuousWithinAt
    (L : ∀ x ∈ s, ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F,
      ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) :
    ContinuousOn f s := fun x hx =>
  continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt hx (L x hx)

Continuity on a Set via Local Uniform Approximation

Informal description

Let $X$ be a topological space, $Y$ a uniform space, and $s \subseteq X$. Suppose that for every $x \in s$ and every entourage $u \in \mathfrak{U}(Y)$, there exists a neighborhood $t$ of $x$ within $s$ and a function $F \colon X \to Y$ such that: 1. $F$ is continuous at $x$ within $s$, and 2. For all $y \in t$, the pair $(f(y), F(y))$ belongs to $u$. Then $f$ is continuous on $s$.

continuousOn_of_uniform_approx_of_continuousOn theorem

(L : ∀ u ∈ 𝓤 β, ∃ F, ContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u) : ContinuousOn f s

Full source

/-- A function which can be uniformly approximated by functions which are continuous on a set
is continuous on this set. -/
theorem continuousOn_of_uniform_approx_of_continuousOn
    (L : ∀ u ∈ 𝓤 β, ∃ F, ContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u) : ContinuousOn f s :=
  continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun _x hx u hu =>
    ⟨s, self_mem_nhdsWithin, (L u hu).imp fun _F hF => ⟨hF.1.continuousWithinAt hx, hF.2⟩⟩

Continuity on a Set via Uniform Approximation by Continuous Functions

Informal description

Let $X$ be a topological space, $Y$ a uniform space, $s \subseteq X$, and $f \colon X \to Y$ a function. Suppose that for every entourage $u \in \mathfrak{U}(Y)$, there exists a function $F \colon X \to Y$ such that: 1. $F$ is continuous on $s$, and 2. For all $y \in s$, the pair $(f(y), F(y))$ belongs to $u$. Then $f$ is continuous on $s$.

continuous_of_locally_uniform_approx_of_continuousAt theorem

 (L : ∀ x : α, ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : Continuous f

Full source

/-- A function which can be locally uniformly approximated by continuous functions is continuous. -/
theorem continuous_of_locally_uniform_approx_of_continuousAt
    (L : ∀ x : α, ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) :
    Continuous f :=
  continuous_iff_continuousAt.2 fun x =>
    continuousAt_of_locally_uniform_approx_of_continuousAt (L x)

Continuity via Local Uniform Approximation

Informal description

Let $X$ be a topological space, $Y$ a uniform space, and $f \colon X \to Y$ a function. Suppose that for every $x \in X$ and every entourage $u \in \mathfrak{U}(Y)$, there exists a neighborhood $t$ of $x$ in $X$ and a function $F \colon X \to Y$ such that: 1. $F$ is continuous at $x$, and 2. For all $y \in t$, the pair $(f(y), F(y))$ belongs to $u$. Then $f$ is continuous on $X$.

continuous_of_uniform_approx_of_continuous theorem

(L : ∀ u ∈ 𝓤 β, ∃ F, Continuous F ∧ ∀ y, (f y, F y) ∈ u) : Continuous f

Full source

/-- A function which can be uniformly approximated by continuous functions is continuous. -/
theorem continuous_of_uniform_approx_of_continuous
    (L : ∀ u ∈ 𝓤 β, ∃ F, Continuous F ∧ ∀ y, (f y, F y) ∈ u) : Continuous f :=
  continuous_iff_continuousOn_univ.mpr <|
    continuousOn_of_uniform_approx_of_continuousOn <| by
      simpa [continuous_iff_continuousOn_univ] using L

Continuity via Uniform Approximation by Continuous Functions

Informal description

Let $X$ be a topological space, $Y$ a uniform space, and $f \colon X \to Y$ a function. Suppose that for every entourage $u \in \mathfrak{U}(Y)$, there exists a continuous function $F \colon X \to Y$ such that for all $y \in X$, the pair $(f(y), F(y))$ belongs to $u$. Then $f$ is continuous.

TendstoLocallyUniformlyOn.continuousOn theorem

(h : TendstoLocallyUniformlyOn F f p s) (hc : ∀ᶠ n in p, ContinuousOn (F n) s) [NeBot p] : ContinuousOn f s

Full source

/-- A locally uniform limit on a set of functions which are continuous on this set is itself
continuous on this set. -/
protected theorem TendstoLocallyUniformlyOn.continuousOn (h : TendstoLocallyUniformlyOn F f p s)
    (hc : ∀ᶠ n in p, ContinuousOn (F n) s) [NeBot p] : ContinuousOn f s := by
  refine continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun x hx u hu => ?_
  rcases h u hu x hx with ⟨t, ht, H⟩
  rcases (hc.and H).exists with ⟨n, hFc, hF⟩
  exact ⟨t, ht, ⟨F n, hFc.continuousWithinAt hx, hF⟩⟩

Continuity of Locally Uniform Limit on a Set

Informal description

Let $X$ be a topological space, $Y$ a uniform space, and $s \subseteq X$. Suppose a sequence of functions $F_n \colon X \to Y$ converges locally uniformly on $s$ to a function $f \colon X \to Y$ with respect to a filter $p$ on the index set. If for all $n$ eventually in $p$, the functions $F_n$ are continuous on $s$, and the filter $p$ is not trivial, then $f$ is continuous on $s$.

TendstoUniformlyOn.continuousOn theorem

(h : TendstoUniformlyOn F f p s) (hc : ∀ᶠ n in p, ContinuousOn (F n) s) [NeBot p] : ContinuousOn f s

Full source

/-- A uniform limit on a set of functions which are continuous on this set is itself continuous
on this set. -/
protected theorem TendstoUniformlyOn.continuousOn (h : TendstoUniformlyOn F f p s)
    (hc : ∀ᶠ n in p, ContinuousOn (F n) s) [NeBot p] : ContinuousOn f s :=
  h.tendstoLocallyUniformlyOn.continuousOn hc

Continuity of Uniform Limit on a Set

Informal description

Let $X$ be a topological space, $Y$ a uniform space, and $s \subseteq X$. Suppose a sequence of functions $F_n \colon X \to Y$ converges uniformly on $s$ to a function $f \colon X \to Y$ with respect to a filter $p$ on the index set. If for all $n$ eventually in $p$, the functions $F_n$ are continuous on $s$, and the filter $p$ is not trivial, then $f$ is continuous on $s$.

TendstoLocallyUniformly.continuous theorem

(h : TendstoLocallyUniformly F f p) (hc : ∀ᶠ n in p, Continuous (F n)) [NeBot p] : Continuous f

Full source

/-- A locally uniform limit of continuous functions is continuous. -/
protected theorem TendstoLocallyUniformly.continuous (h : TendstoLocallyUniformly F f p)
    (hc : ∀ᶠ n in p, Continuous (F n)) [NeBot p] : Continuous f :=
  continuous_iff_continuousOn_univ.mpr <|
    h.tendstoLocallyUniformlyOn.continuousOn <| hc.mono fun _n hn => hn.continuousOn

Continuity of Locally Uniform Limit

Informal description

Let $X$ be a topological space and $Y$ a uniform space. Suppose a sequence of functions $F_n \colon X \to Y$ converges locally uniformly to a function $f \colon X \to Y$ with respect to a filter $p$ on the index set. If for all $n$ eventually in $p$, the functions $F_n$ are continuous, and the filter $p$ is not trivial, then $f$ is continuous.

TendstoUniformly.continuous theorem

(h : TendstoUniformly F f p) (hc : ∀ᶠ n in p, Continuous (F n)) [NeBot p] : Continuous f

Full source

/-- A uniform limit of continuous functions is continuous. -/
protected theorem TendstoUniformly.continuous (h : TendstoUniformly F f p)
    (hc : ∀ᶠ n in p, Continuous (F n)) [NeBot p] : Continuous f :=
  h.tendstoLocallyUniformly.continuous hc

Continuity of Uniform Limit

Informal description

Let $X$ be a topological space and $Y$ a uniform space. Suppose a sequence of functions $F_n \colon X \to Y$ converges uniformly to a function $f \colon X \to Y$ with respect to a filter $p$ on the index set. If for all $n$ eventually in $p$, the functions $F_n$ are continuous, and the filter $p$ is not trivial, then $f$ is continuous.

tendsto_comp_of_locally_uniform_limit_within theorem

 (h : ContinuousWithinAt f s x) (hg : Tendsto g p (𝓝[s] x))
  (hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) : Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Full source

/-- 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_within (h : ContinuousWithinAt f s x)
    (hg : Tendsto g p (𝓝[s] x))
    (hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) :
    Tendsto (fun n => F n (g n)) p (𝓝 (f x)) := by
  refine Uniform.tendsto_nhds_right.2 fun u₀ hu₀ => ?_
  obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
  rcases hunif u₁ h₁ with ⟨s, sx, hs⟩
  have A : ∀ᶠ n in p, g n ∈ s := hg sx
  have B : ∀ᶠ n in p, (f x, f (g n)) ∈ u₁ := hg (Uniform.continuousWithinAt_iff'_right.1 h h₁)
  exact B.mp <| A.mp <| hs.mono fun y H1 H2 H3 => u₁₀ (prodMk_mem_compRel H3 (H1 _ H2))

Limit of compositions under locally uniform convergence within a set

Informal description

Let $X$ be a topological space, $Y$ a uniform space, $s \subseteq X$, $x \in X$, and $p$ a filter. Suppose: 1. $f : X \to Y$ is continuous at $x$ within $s$, 2. $g : \alpha \to X$ tends to $x$ within $s$ along $p$, 3. For every entourage $u$ in the uniformity of $Y$, there exists a neighborhood $t$ of $x$ within $s$ such that for $p$-eventually all $n$, for all $y \in t$, $(f(y), F_n(y)) \in u$. Then the composition $(F_n \circ g)_n$ tends to $f(x)$ along $p$.

tendsto_comp_of_locally_uniform_limit theorem

 (h : ContinuousAt f x) (hg : Tendsto g p (𝓝 x)) (hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) :
  Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Full source

/-- 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 tendsto_comp_of_locally_uniform_limit (h : ContinuousAt f x) (hg : Tendsto g p (𝓝 x))
    (hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) :
    Tendsto (fun n => F n (g n)) p (𝓝 (f x)) := by
  rw [← continuousWithinAt_univ] at h
  rw [← nhdsWithin_univ] at hunif hg
  exact tendsto_comp_of_locally_uniform_limit_within h hg hunif

Limit of compositions under locally uniform convergence

Informal description

Let $X$ be a topological space, $Y$ a uniform space, $x \in X$, and $p$ a filter. Suppose: 1. $f \colon X \to Y$ is continuous at $x$, 2. $g \colon \alpha \to X$ tends to $x$ along $p$, 3. For every entourage $u$ in the uniformity of $Y$, there exists a neighborhood $t$ of $x$ such that for $p$-eventually all $n$, for all $y \in t$, $(f(y), F_n(y)) \in u$. Then the composition $(F_n \circ g)_n$ tends to $f(x)$ along $p$.

TendstoLocallyUniformlyOn.tendsto_comp theorem

 (h : TendstoLocallyUniformlyOn F f p s) (hf : ContinuousWithinAt f s x) (hx : x ∈ s) (hg : Tendsto g p (𝓝[s] x)) :
  Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Full source

/-- 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 TendstoLocallyUniformlyOn.tendsto_comp (h : TendstoLocallyUniformlyOn F f p s)
    (hf : ContinuousWithinAt f s x) (hx : x ∈ s) (hg : Tendsto g p (𝓝[s] x)) :
    Tendsto (fun n => F n (g n)) p (𝓝 (f x)) :=
  tendsto_comp_of_locally_uniform_limit_within hf hg fun u hu => h u hu x hx

Limit of Function Compositions under Locally Uniform Convergence on a Set

Informal description

Let $X$ be a topological space, $Y$ a uniform space, $s \subseteq X$, $x \in s$, and $p$ a filter on an index set. Suppose: 1. The sequence of functions $F_n \colon X \to Y$ converges locally uniformly to $f \colon X \to Y$ on $s$ along $p$, 2. $f$ is continuous at $x$ within $s$, 3. The sequence $g_n \colon \alpha \to X$ tends to $x$ within $s$ along $p$. Then the sequence $(F_n(g_n))_n$ tends to $f(x)$ along $p$.

TendstoUniformlyOn.tendsto_comp theorem

 (h : TendstoUniformlyOn F f p s) (hf : ContinuousWithinAt f s x) (hg : Tendsto g p (𝓝[s] x)) :
  Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Full source

/-- 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 TendstoUniformlyOn.tendsto_comp (h : TendstoUniformlyOn F f p s)
    (hf : ContinuousWithinAt f s x) (hg : Tendsto g p (𝓝[s] x)) :
    Tendsto (fun n => F n (g n)) p (𝓝 (f x)) :=
  tendsto_comp_of_locally_uniform_limit_within hf hg fun u hu => ⟨s, self_mem_nhdsWithin, h u hu⟩

Limit of compositions under uniform convergence on a set

Informal description

Let $X$ be a topological space, $Y$ a uniform space, $s \subseteq X$, $x \in X$, and $p$ a filter. Suppose: 1. The sequence of functions $F_n : X \to Y$ converges uniformly to $f : X \to Y$ on $s$ along $p$, 2. $f$ is continuous at $x$ within $s$, 3. The sequence $g_n : \alpha \to X$ tends to $x$ within $s$ along $p$. Then the sequence $(F_n(g_n))_n$ converges to $f(x)$ along $p$.

TendstoLocallyUniformly.tendsto_comp theorem

 (h : TendstoLocallyUniformly F f p) (hf : ContinuousAt f x) (hg : Tendsto g p (𝓝 x)) :
  Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Full source

/-- If `Fₙ` tends locally uniformly to `f`, and `gₙ` tends to `x`, then `Fₙ gₙ` tends to `f x`. -/
theorem TendstoLocallyUniformly.tendsto_comp (h : TendstoLocallyUniformly F f p)
    (hf : ContinuousAt f x) (hg : Tendsto g p (𝓝 x)) : Tendsto (fun n => F n (g n)) p (𝓝 (f x)) :=
  tendsto_comp_of_locally_uniform_limit hf hg fun u hu => h u hu x

Limit of compositions under locally uniform convergence

Informal description

Let $X$ be a topological space, $Y$ a uniform space, $x \in X$, and $p$ a filter on an index set. Suppose: 1. The sequence of functions $F_n \colon X \to Y$ converges locally uniformly to $f \colon X \to Y$ along $p$, 2. $f$ is continuous at $x$, 3. The sequence $g_n \colon \alpha \to X$ tends to $x$ along $p$. Then the sequence $(F_n(g_n))_n$ converges to $f(x)$ along $p$.

TendstoUniformly.tendsto_comp theorem

 (h : TendstoUniformly F f p) (hf : ContinuousAt f x) (hg : Tendsto g p (𝓝 x)) :
  Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Full source

/-- If `Fₙ` tends uniformly to `f`, and `gₙ` tends to `x`, then `Fₙ gₙ` tends to `f x`. -/
theorem TendstoUniformly.tendsto_comp (h : TendstoUniformly F f p) (hf : ContinuousAt f x)
    (hg : Tendsto g p (𝓝 x)) : Tendsto (fun n => F n (g n)) p (𝓝 (f x)) :=
  h.tendstoLocallyUniformly.tendsto_comp hf hg

Limit of Compositions under Uniform Convergence

Informal description

Let $X$ be a topological space, $Y$ a uniform space, $x \in X$, and $p$ a filter on an index set. Suppose: 1. The sequence of functions $F_n \colon X \to Y$ converges uniformly to $f \colon X \to Y$ along $p$, 2. $f$ is continuous at $x$, 3. The sequence $g_n \colon \alpha \to X$ tends to $x$ along $p$. Then the sequence $(F_n(g_n))_n$ converges to $f(x)$ along $p$.