Mathlib.Topology.UniformSpace.LocallyUniformConvergence

TendstoLocallyUniformlyOn definition

(F : ι → α → β) (f : α → β) (p : Filter ι) (s : Set α)

Full source

/-- 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`. -/
def TendstoLocallyUniformlyOn (F : ι → α → β) (f : α → β) (p : Filter ι) (s : Set α) :=
  ∀ u ∈ 𝓤 β, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u

Locally uniform convergence on a set

Informal description

A sequence of functions $ F_n \colon \alpha \to \beta $ converges locally uniformly on a set $ s \subseteq \alpha $ to a function $ f \colon \alpha \to \beta $ with respect to a filter $ p $ on the index set $ \iota $ if, for every entourage $ u $ of the diagonal in $ \beta \times \beta $ and every $ x \in s $, there exists a neighborhood $ t $ of $ x $ in $ s $ such that for all $ n $ eventually in $ p $, the pair $ (f(y), F_n(y)) $ lies in $ u $ for all $ y \in t $.

TendstoLocallyUniformly definition

(F : ι → α → β) (f : α → β) (p : Filter ι)

Full source

/-- 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`. -/
def TendstoLocallyUniformly (F : ι → α → β) (f : α → β) (p : Filter ι) :=
  ∀ u ∈ 𝓤 β, ∀ x : α, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u

Locally uniform convergence of a sequence of functions

Informal description

A sequence of functions $ F_n \colon \alpha \to \beta $ converges locally uniformly to a function $ f \colon \alpha \to \beta $ with respect to a filter $ p $ on the index set $ \iota $ if, for every entourage $ u $ of the diagonal in $ \beta \times \beta $ and every $ x \in \alpha $, there exists a neighborhood $ t $ of $ x $ such that for all $ n $ eventually in $ p $, the pair $ (f(y), F_n(y)) $ lies in $ u $ for all $ y \in t $.

tendstoLocallyUniformlyOn_univ theorem

: TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p

Full source

theorem tendstoLocallyUniformlyOn_univ :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p := by
  simp [TendstoLocallyUniformlyOn, TendstoLocallyUniformly, nhdsWithin_univ]

Equivalence of Local Uniform Convergence on Entire Space and Local Uniform Convergence on Universal Set

Informal description

A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly on the entire space $\alpha$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if it converges locally uniformly to $f$ on the set $\text{univ} = \alpha$ with respect to $p$.

tendstoLocallyUniformlyOn_iff_forall_tendsto theorem

 : TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Full source

theorem tendstoLocallyUniformlyOn_iff_forall_tendsto :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔
      ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β) :=
  forall₂_swap.trans <| forall₄_congr fun _ _ _ _ => by
    rw [mem_map, mem_prod_iff_right]; rfl

Characterization of Locally Uniform Convergence on a Set via Pointwise Tendency to the Diagonal

Informal description

A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly on a set $s \subseteq \alpha$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if for every $x \in s$, the map $(n, y) \mapsto (f(y), F_n(y))$ tends to the diagonal in $\beta \times \beta$ as $n$ tends to $p$ and $y$ tends to $x$ within $s$.

IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto theorem

 (hs : IsOpen s) :
  TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Full source

nonrec theorem IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto (hs : IsOpen s) :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔
      ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β) :=
  tendstoLocallyUniformlyOn_iff_forall_tendsto.trans <| forall₂_congr fun x hx => by
    rw [hs.nhdsWithin_eq hx]

Characterization of locally uniform convergence on open sets via pointwise convergence to the diagonal

Informal description

Let $s$ be an open subset of a topological space $\alpha$. A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly on $s$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if for every $x \in s$, the map $(n, y) \mapsto (f(y), F_n(y))$ tends to the diagonal in $\beta \times \beta$ as $n$ tends to $p$ and $y$ tends to $x$.

tendstoLocallyUniformly_iff_forall_tendsto theorem

: TendstoLocallyUniformly F f p ↔ ∀ x, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Full source

theorem tendstoLocallyUniformly_iff_forall_tendsto :
    TendstoLocallyUniformlyTendstoLocallyUniformly F f p ↔
      ∀ x, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β) := by
  simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]

Characterization of Locally Uniform Convergence via Pointwise Tendency to the Diagonal

Informal description

A sequence of functions $ F_n \colon \alpha \to \beta $ converges locally uniformly to a function $ f \colon \alpha \to \beta $ with respect to a filter $ p $ if and only if for every point $ x \in \alpha $, the map $(n, y) \mapsto (f(y), F_n(y))$ tends to the diagonal in $\beta \times \beta$ as $ n $ tends to $ p $ and $ y $ tends to $ x $.

tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe theorem

: TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p

Full source

theorem tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔
      TendstoLocallyUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p := by
  simp only [tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendsto_map'_iff,
    tendstoLocallyUniformlyOn_iff_forall_tendsto, ← map_nhds_subtype_val, prod_map_right]; rfl

Equivalence of locally uniform convergence on a set and locally uniform convergence of restrictions

Informal description

A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly on a set $s \subseteq \alpha$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if the sequence of restricted functions $F_n \restriction s$ converges locally uniformly to $f \restriction s$ with respect to $p$.

TendstoUniformlyOn.tendstoLocallyUniformlyOn theorem

(h : TendstoUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p s

Full source

protected theorem TendstoUniformlyOn.tendstoLocallyUniformlyOn (h : TendstoUniformlyOn F f p s) :
    TendstoLocallyUniformlyOn F f p s := fun u hu _ _ =>
  ⟨s, self_mem_nhdsWithin, by simpa using h u hu⟩

Uniform convergence implies locally uniform convergence on a set

Informal description

If a sequence of functions $F_n$ converges uniformly to $f$ on a set $s$ with respect to a filter $p$, then $F_n$ also converges locally uniformly to $f$ on $s$ with respect to $p$.

TendstoUniformly.tendstoLocallyUniformly theorem

(h : TendstoUniformly F f p) : TendstoLocallyUniformly F f p

Full source

protected theorem TendstoUniformly.tendstoLocallyUniformly (h : TendstoUniformly F f p) :
    TendstoLocallyUniformly F f p := fun u hu _ => ⟨univ, univ_mem, by simpa using h u hu⟩

Uniform Convergence Implies Locally Uniform Convergence

Informal description

If a sequence of functions $ F_n \colon \alpha \to \beta $ converges uniformly to a function $ f \colon \alpha \to \beta $ with respect to a filter $ p $ on the index set, then $ F_n $ also converges locally uniformly to $ f $ with respect to $ p $.

TendstoLocallyUniformlyOn.mono theorem

(h : TendstoLocallyUniformlyOn F f p s) (h' : s' ⊆ s) : TendstoLocallyUniformlyOn F f p s'

Full source

theorem TendstoLocallyUniformlyOn.mono (h : TendstoLocallyUniformlyOn F f p s) (h' : s' ⊆ s) :
    TendstoLocallyUniformlyOn F f p s' := by
  intro u hu x hx
  rcases h u hu x (h' hx) with ⟨t, ht, H⟩
  exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩

Local Uniform Convergence is Monotonic with Respect to Subsets

Informal description

If a sequence of functions $F_n$ converges locally uniformly to $f$ on a set $s$ with respect to a filter $p$, then for any subset $s' \subseteq s$, the sequence $F_n$ also converges locally uniformly to $f$ on $s'$ with respect to $p$.

tendstoLocallyUniformlyOn_iUnion theorem

 {ι' : Sort*} {S : ι' → Set α} (hS : ∀ i, IsOpen (S i)) (h : ∀ i, TendstoLocallyUniformlyOn F f p (S i)) :
  TendstoLocallyUniformlyOn F f p (⋃ i, S i)

Full source

theorem tendstoLocallyUniformlyOn_iUnion {ι' : Sort*} {S : ι' → Set α} (hS : ∀ i, IsOpen (S i))
    (h : ∀ i, TendstoLocallyUniformlyOn F f p (S i)) :
    TendstoLocallyUniformlyOn F f p (⋃ i, S i) :=
  (isOpen_iUnion hS).tendstoLocallyUniformlyOn_iff_forall_tendsto.2 fun _x hx =>
    let ⟨i, hi⟩ := mem_iUnion.1 hx
    (hS i).tendstoLocallyUniformlyOn_iff_forall_tendsto.1 (h i) _ hi

Locally Uniform Convergence on Union of Open Sets

Informal description

Let $\{S_i\}_{i \in \iota'}$ be a family of open subsets of a topological space $\alpha$. If a sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to $f \colon \alpha \to \beta$ on each $S_i$ with respect to a filter $p$, then $F_n$ converges locally uniformly to $f$ on the union $\bigcup_i S_i$ with respect to $p$.

tendstoLocallyUniformlyOn_biUnion theorem

 {s : Set γ} {S : γ → Set α} (hS : ∀ i ∈ s, IsOpen (S i)) (h : ∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i)) :
  TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i)

Full source

theorem tendstoLocallyUniformlyOn_biUnion {s : Set γ} {S : γ → Set α} (hS : ∀ i ∈ s, IsOpen (S i))
    (h : ∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i)) :
    TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i) :=
  tendstoLocallyUniformlyOn_iUnion (fun i => isOpen_iUnion (hS i)) fun i =>
   tendstoLocallyUniformlyOn_iUnion (hS i) (h i)

Locally Uniform Convergence on Union of Open Sets Indexed by a Set

Informal description

Let $s$ be a set of indices and $\{S_i\}_{i \in s}$ be a family of open subsets of a topological space $\alpha$. If a sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to $f \colon \alpha \to \beta$ on each $S_i$ for $i \in s$ with respect to a filter $p$, then $F_n$ converges locally uniformly to $f$ on the union $\bigcup_{i \in s} S_i$ with respect to $p$.

tendstoLocallyUniformlyOn_sUnion theorem

 (S : Set (Set α)) (hS : ∀ s ∈ S, IsOpen s) (h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s) :
  TendstoLocallyUniformlyOn F f p (⋃₀ S)

Full source

theorem tendstoLocallyUniformlyOn_sUnion (S : Set (Set α)) (hS : ∀ s ∈ S, IsOpen s)
    (h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p (⋃₀ S) := by
  rw [sUnion_eq_biUnion]
  exact tendstoLocallyUniformlyOn_biUnion hS h

Locally Uniform Convergence on Union of Open Sets in a Family

Informal description

Let $S$ be a set of subsets of a topological space $\alpha$ such that every $s \in S$ is open. Suppose a sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to a function $f \colon \alpha \to \beta$ on each $s \in S$ with respect to a filter $p$. Then $F_n$ converges locally uniformly to $f$ on the union $\bigcup_{s \in S} s$ with respect to $p$.

TendstoLocallyUniformlyOn.union theorem

 (hs₁ : IsOpen s) (hs₂ : IsOpen s') (h₁ : TendstoLocallyUniformlyOn F f p s) (h₂ : TendstoLocallyUniformlyOn F f p s') :
  TendstoLocallyUniformlyOn F f p (s ∪ s')

Full source

theorem TendstoLocallyUniformlyOn.union (hs₁ : IsOpen s) (hs₂ : IsOpen s')
    (h₁ : TendstoLocallyUniformlyOn F f p s) (h₂ : TendstoLocallyUniformlyOn F f p s') :
    TendstoLocallyUniformlyOn F f p (s ∪ s') := by
  rw [← sUnion_pair]
  refine tendstoLocallyUniformlyOn_sUnion _ ?_ ?_ <;> simp [*]

Local Uniform Convergence on Union of Open Sets

Informal description

Let $s$ and $s'$ be open subsets of a topological space $\alpha$. If a sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to a function $f \colon \alpha \to \beta$ on both $s$ and $s'$ with respect to a filter $p$, then $F_n$ converges locally uniformly to $f$ on the union $s \cup s'$ with respect to $p$.

TendstoLocallyUniformly.tendstoLocallyUniformlyOn theorem

(h : TendstoLocallyUniformly F f p) : TendstoLocallyUniformlyOn F f p s

Full source

protected theorem TendstoLocallyUniformly.tendstoLocallyUniformlyOn
    (h : TendstoLocallyUniformly F f p) : TendstoLocallyUniformlyOn F f p s :=
  (tendstoLocallyUniformlyOn_univ.mpr h).mono (subset_univ _)

Local uniform convergence implies local uniform convergence on any subset

Informal description

If a sequence of functions $ F_n \colon \alpha \to \beta $ converges locally uniformly to a function $ f \colon \alpha \to \beta $ with respect to a filter $ p $, then for any subset $ s \subseteq \alpha $, the sequence $ F_n $ also converges locally uniformly to $ f $ on $ s $ with respect to $ p $.

tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace theorem

[CompactSpace α] : TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Full source

/-- On a compact space, locally uniform convergence is just uniform convergence. -/
theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace [CompactSpace α] :
    TendstoLocallyUniformlyTendstoLocallyUniformly F f p ↔ TendstoUniformly F f p := by
  refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩
  choose U hU using h V hV
  obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1
  replace hU := fun x : t => (hU x).2
  rw [← eventually_all] at hU
  refine hU.mono fun i hi x => ?_
  specialize ht (mem_univ x)
  simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right, Subtype.coe_mk] at ht
  obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht
  exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃

Equivalence of Local and Uniform Convergence on Compact Spaces

Informal description

Let $\alpha$ be a compact topological space. A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if $F_n$ converges uniformly to $f$ with respect to $p$.

tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact theorem

(hs : IsCompact s) : TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

Full source

/-- For a compact set `s`, locally uniform convergence on `s` is just uniform convergence on `s`. -/
theorem tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact (hs : IsCompact s) :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s := by
  haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
  refine ⟨fun h => ?_, TendstoUniformlyOn.tendstoLocallyUniformlyOn⟩
  rwa [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,
    tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, ←
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe] at h

Equivalence of locally uniform and uniform convergence on compact sets

Informal description

For a compact subset $s$ of a topological space, a sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly on $s$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if $F_n$ converges uniformly to $f$ on $s$ with respect to $p$.

TendstoLocallyUniformlyOn.comp theorem

 [TopologicalSpace γ] {t : Set γ} (h : TendstoLocallyUniformlyOn F f p s) (g : γ → α) (hg : MapsTo g t s)
  (cg : ContinuousOn g t) : TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p t

Full source

theorem TendstoLocallyUniformlyOn.comp [TopologicalSpace γ] {t : Set γ}
    (h : TendstoLocallyUniformlyOn F f p s) (g : γ → α) (hg : MapsTo g t s)
    (cg : ContinuousOn g t) : TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p t := by
  intro u hu x hx
  rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩
  have : g ⁻¹' ag ⁻¹' a ∈ 𝓝[t] x :=
    (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)
  exact ⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩

Composition Preserves Locally Uniform Convergence on a Set

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be topological spaces, and let $s \subseteq \alpha$ and $t \subseteq \gamma$ be subsets. Suppose a sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly on $s$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on the index set. If $g \colon \gamma \to \alpha$ is a continuous function on $t$ such that $g(t) \subseteq s$, then the sequence of composed functions $F_n \circ g$ converges locally uniformly on $t$ to $f \circ g$ with respect to the same filter $p$.

TendstoLocallyUniformly.comp theorem

 [TopologicalSpace γ] (h : TendstoLocallyUniformly F f p) (g : γ → α) (cg : Continuous g) :
  TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p

Full source

theorem TendstoLocallyUniformly.comp [TopologicalSpace γ] (h : TendstoLocallyUniformly F f p)
    (g : γ → α) (cg : Continuous g) : TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p := by
  rw [← tendstoLocallyUniformlyOn_univ] at h ⊢
  rw [continuous_iff_continuousOn_univ] at cg
  exact h.comp _ (mapsTo_univ _ _) cg

Composition Preserves Locally Uniform Convergence

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be topological spaces. If a sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on the index set, and $g \colon \gamma \to \alpha$ is a continuous function, then the sequence of composed functions $F_n \circ g$ converges locally uniformly to $f \circ g$ with respect to the same filter $p$.

tendstoLocallyUniformlyOn_TFAE theorem

 [LocallyCompactSpace α] (G : ι → α → β) (g : α → β) (p : Filter ι) (hs : IsOpen s) :
  List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v]

Full source

theorem tendstoLocallyUniformlyOn_TFAE [LocallyCompactSpace α] (G : ι → α → β) (g : α → β)
    (p : Filter ι) (hs : IsOpen s) :
    List.TFAE [
      TendstoLocallyUniformlyOn G g p s,
      ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v] := by
  tfae_have 1 → 2
  | h, K, hK1, hK2 =>
    (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1)
  tfae_have 2 → 3
  | h, x, hx => by
    obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
    exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩
  tfae_have 3 → 1
  | h, u, hu, x, hx => by
    obtain ⟨v, hv1, hv2⟩ := h x hx
    exact ⟨v, hv1, hv2 u hu⟩
  tfae_finish

Equivalent Characterizations of Locally Uniform Convergence on Open Subsets of Locally Compact Spaces

Informal description

Let $\alpha$ be a locally compact space, $s \subseteq \alpha$ an open subset, and $\beta$ a topological space. Consider a sequence of functions $G_n \colon \alpha \to \beta$ and a function $g \colon \alpha \to \beta$. The following statements are equivalent: 1. The sequence $G_n$ converges locally uniformly to $g$ on $s$ with respect to a filter $p$. 2. For every compact subset $K \subseteq s$, the sequence $G_n$ converges uniformly to $g$ on $K$ with respect to $p$. 3. For every $x \in s$, there exists a neighborhood $v$ of $x$ in $s$ such that $G_n$ converges uniformly to $g$ on $v$ with respect to $p$.

tendstoLocallyUniformlyOn_iff_forall_isCompact theorem

 [LocallyCompactSpace α] (hs : IsOpen s) :
  TendstoLocallyUniformlyOn F f p s ↔ ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn F f p K

Full source

theorem tendstoLocallyUniformlyOn_iff_forall_isCompact [LocallyCompactSpace α] (hs : IsOpen s) :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔ ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn F f p K :=
  (tendstoLocallyUniformlyOn_TFAE F f p hs).out 0 1

Characterization of Locally Uniform Convergence on Open Subsets via Compact Subsets

Informal description

Let $\alpha$ be a locally compact space and $s \subseteq \alpha$ an open subset. A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to $f \colon \alpha \to \beta$ on $s$ with respect to a filter $p$ if and only if for every compact subset $K \subseteq s$, the sequence $F_n$ converges uniformly to $f$ on $K$ with respect to $p$.

tendstoLocallyUniformly_iff_forall_isCompact theorem

[LocallyCompactSpace α] : TendstoLocallyUniformly F f p ↔ ∀ K : Set α, IsCompact K → TendstoUniformlyOn F f p K

Full source

lemma tendstoLocallyUniformly_iff_forall_isCompact [LocallyCompactSpace α]  :
    TendstoLocallyUniformlyTendstoLocallyUniformly F f p ↔ ∀ K : Set α, IsCompact K → TendstoUniformlyOn F f p K := by
  simp only [← tendstoLocallyUniformlyOn_univ,
    tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_univ, Set.subset_univ, forall_true_left]

Characterization of Locally Uniform Convergence via Compact Subsets in Locally Compact Spaces

Informal description

Let $\alpha$ be a locally compact space. A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if for every compact subset $K \subseteq \alpha$, the sequence $F_n$ converges uniformly to $f$ on $K$ with respect to $p$.

tendstoLocallyUniformlyOn_iff_filter theorem

: TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)

Full source

theorem tendstoLocallyUniformlyOn_iff_filter :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x) := by
  simp only [TendstoUniformlyOnFilter, eventually_prod_iff]
  constructor
  · rintro h x hx u hu
    obtain ⟨s, hs1, hs2⟩ := h u hu x hx
    exact ⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩
  · rintro h u hu x hx
    obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu
    exact ⟨pb, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩

Characterization of Locally Uniform Convergence on a Set via Filter Convergence

Informal description

A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly on a set $s \subseteq \alpha$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if for every $x \in s$, the sequence $F_n$ converges uniformly to $f$ on the neighborhood filter of $x$ restricted to $s$ (denoted $\mathcal{N}_s(x)$).

tendstoLocallyUniformly_iff_filter theorem

: TendstoLocallyUniformly F f p ↔ ∀ x, TendstoUniformlyOnFilter F f p (𝓝 x)

Full source

theorem tendstoLocallyUniformly_iff_filter :
    TendstoLocallyUniformlyTendstoLocallyUniformly F f p ↔ ∀ x, TendstoUniformlyOnFilter F f p (𝓝 x) := by
  simpa [← tendstoLocallyUniformlyOn_univ, ← nhdsWithin_univ] using
    @tendstoLocallyUniformlyOn_iff_filter _ _ _ _ _ F f univ p

Characterization of Locally Uniform Convergence via Filter Convergence

Informal description

A sequence of functions $F_n \colon \alpha \to \beta$ converges locally uniformly to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ if and only if for every $x \in \alpha$, the sequence $F_n$ converges uniformly to $f$ on the neighborhood filter of $x$ (denoted $\mathcal{N}(x)$).

TendstoLocallyUniformlyOn.tendsto_at theorem

(hf : TendstoLocallyUniformlyOn F f p s) {a : α} (ha : a ∈ s) : Tendsto (fun i => F i a) p (𝓝 (f a))

Full source

theorem TendstoLocallyUniformlyOn.tendsto_at (hf : TendstoLocallyUniformlyOn F f p s) {a : α}
    (ha : a ∈ s) : Tendsto (fun i => F i a) p (𝓝 (f a)) := by
  refine ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_
  simpa only [Filter.principal_singleton] using pure_le_nhdsWithin ha

Pointwise Convergence from Local Uniform Convergence

Informal description

Let $F_n \colon \alpha \to \beta$ be a sequence of functions converging locally uniformly on a set $s \subseteq \alpha$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on the index set. Then for any point $a \in s$, the sequence $F_n(a)$ converges to $f(a)$ in the neighborhood filter of $a$.

TendstoLocallyUniformlyOn.unique theorem

 [p.NeBot] [T2Space β] {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : TendstoLocallyUniformlyOn F g p s) :
  s.EqOn f g

Full source

theorem TendstoLocallyUniformlyOn.unique [p.NeBot] [T2Space β] {g : α → β}
    (hf : TendstoLocallyUniformlyOn F f p s) (hg : TendstoLocallyUniformlyOn F g p s) :
    s.EqOn f g := fun _a ha => tendsto_nhds_unique (hf.tendsto_at ha) (hg.tendsto_at ha)

Uniqueness of Locally Uniform Limits in Hausdorff Spaces

Informal description

Let $β$ be a Hausdorff space, $p$ a non-trivial filter, and $F_n \colon α \to β$ a sequence of functions. If $F_n$ converges locally uniformly to both $f$ and $g$ on a set $s \subseteq α$ with respect to $p$, then $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$).

TendstoLocallyUniformlyOn.congr theorem

 {G : ι → α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : ∀ n, s.EqOn (F n) (G n)) :
  TendstoLocallyUniformlyOn G f p s

Full source

theorem TendstoLocallyUniformlyOn.congr {G : ι → α → β} (hf : TendstoLocallyUniformlyOn F f p s)
    (hg : ∀ n, s.EqOn (F n) (G n)) : TendstoLocallyUniformlyOn G f p s := by
  rintro u hu x hx
  obtain ⟨t, ht, h⟩ := hf u hu x hx
  refine ⟨s ∩ t, inter_mem self_mem_nhdsWithin ht, ?_⟩
  filter_upwards [h] with i hi y hy using hg i hy.1 ▸ hi y hy.2

Local Uniform Convergence is Preserved Under Pointwise Equality on the Domain

Informal description

Let $F_n \colon \alpha \to \beta$ be a sequence of functions converging locally uniformly on a set $s \subseteq \alpha$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on the index set $\iota$. If for each $n$, the functions $F_n$ and $G_n$ agree on $s$ (i.e., $F_n(y) = G_n(y)$ for all $y \in s$), then $G_n$ also converges locally uniformly to $f$ on $s$ with respect to $p$.

TendstoLocallyUniformlyOn.congr_right theorem

{g : α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : s.EqOn f g) : TendstoLocallyUniformlyOn F g p s

Full source

theorem TendstoLocallyUniformlyOn.congr_right {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s)
    (hg : s.EqOn f g) : TendstoLocallyUniformlyOn F g p s := by
  rintro u hu x hx
  obtain ⟨t, ht, h⟩ := hf u hu x hx
  refine ⟨s ∩ t, inter_mem self_mem_nhdsWithin ht, ?_⟩
  filter_upwards [h] with i hi y hy using hg hy.1 ▸ hi y hy.2

Local Uniform Convergence is Preserved Under Pointwise Equality on the Subset

Informal description

Let $F_n \colon \alpha \to \beta$ be a sequence of functions, $f, g \colon \alpha \to \beta$ be functions, $p$ be a filter on the index set, and $s \subseteq \alpha$ be a subset. If $F_n$ converges locally uniformly to $f$ on $s$ with respect to $p$, and $f$ coincides with $g$ on $s$, then $F_n$ also converges locally uniformly to $g$ on $s$ with respect to $p$.

Tags