Locally uniform convergence

We define a sequence of functions Fₙ to converge locally uniformly to a limiting function f with respect to a filter p, spelled TendstoLocallyUniformly F f p, if for any x ∈ s and any entourage of the diagonal u, there is a neighbourhood v of x such that p-eventually we have (f y, Fₙ y) ∈ u for all y ∈ v.

It is important to note that this definition is somewhat non-standard; it is not in general equivalent to "every point has a neighborhood on which the convergence is uniform", which is the definition more commonly encountered in the literature. The reason is that in our definition the neighborhood v of x can depend on the entourage u; so our condition is a priori weaker than the usual one, although the two conditions are equivalent if the domain is locally compact. See tendstoLocallyUniformlyOn_of_forall_exists_nhds for the one-way implication; the equivalence assuming local compactness is part of tendstoLocallyUniformlyOn_TFAE.

We adopt this weaker condition because it is more general but appears to be sufficient for the standard applications of locally-uniform convergence (in particular, for proving that a locally-uniform limit of continuous functions is continuous).

We also define variants for locally uniform convergence on a subset, called TendstoLocallyUniformlyOn F f p s.

Tags

Uniform limit, uniform convergence, tends uniformly to

def TendstoLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι) (s : Set α) : Prop

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.

Equations

• TendstoLocallyUniformlyOn F f p s = ∀ u ∈ uniformity β, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

def TendstoLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι) : Prop

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.

Equations

• TendstoLocallyUniformly F f p = ∀ u ∈ uniformity β, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

theorem tendstoLocallyUniformlyOn_univ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoLocallyUniformlyOn F f p Set.univ ↔ TendstoLocallyUniformly F f p

theorem tendstoLocallyUniformlyOn_iff_forall_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhdsWithin x s) (uniformity β)

theorem IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (hs : IsOpen s) : TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhds x) (uniformity β)

theorem tendstoLocallyUniformly_iff_forall_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ (x : α), Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhds x) (uniformity β)

theorem tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun (i : ι) (x : ↑s) => F i ↑x) (f ∘ Subtype.val) p

theorem TendstoUniformlyOn.tendstoLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p s

theorem TendstoUniformly.tendstoLocallyUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : TendstoUniformly F f p) : TendstoLocallyUniformly F f p

theorem TendstoLocallyUniformlyOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s s' : Set α} {p : Filter ι} (h : TendstoLocallyUniformlyOn F f p s) (h' : s' ⊆ s) : TendstoLocallyUniformlyOn F f p s'

theorem tendstoLocallyUniformlyOn_iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {ι' : Sort u_5} {S : ι' → Set α} (hS : ∀ (i : ι'), IsOpen (S i)) (h : ∀ (i : ι'), TendstoLocallyUniformlyOn F f p (S i)) : TendstoLocallyUniformlyOn F f p (⋃ (i : ι'), S i)

theorem tendstoLocallyUniformlyOn_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {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)

theorem tendstoLocallyUniformlyOn_sUnion {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (S : Set (Set α)) (hS : ∀ s ∈ S, IsOpen s) (h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p (⋃₀ S)

theorem TendstoLocallyUniformlyOn.union {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s s' : Set α} {p : Filter ι} (hs₁ : IsOpen s) (hs₂ : IsOpen s') (h₁ : TendstoLocallyUniformlyOn F f p s) (h₂ : TendstoLocallyUniformlyOn F f p s') : TendstoLocallyUniformlyOn F f p (s ∪ s')

theorem TendstoLocallyUniformly.tendstoLocallyUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoLocallyUniformly F f p) : TendstoLocallyUniformlyOn F f p s

theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [CompactSpace α] : TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

On a compact space, locally uniform convergence is just uniform convergence.

theorem tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (hs : IsCompact s) : TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

For a compact set s, locally uniform convergence on s is just uniform convergence on s.

theorem TendstoLocallyUniformlyOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace γ] {t : Set γ} (h : TendstoLocallyUniformlyOn F f p s) (g : γ → α) (hg : Set.MapsTo g t s) (cg : ContinuousOn g t) : TendstoLocallyUniformlyOn (fun (n : ι) => F n ∘ g) (f ∘ g) p t

theorem TendstoLocallyUniformly.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace γ] (h : TendstoLocallyUniformly F f p) (g : γ → α) (cg : Continuous g) : TendstoLocallyUniformly (fun (n : ι) => F n ∘ g) (f ∘ g) p

theorem tendstoLocallyUniformlyOn_of_forall_exists_nhds {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, TendstoUniformlyOn F f p t) : TendstoLocallyUniformlyOn F f p s

If every x ∈ s has a neighbourhood within s on which F i tends uniformly to f, then F i tends locally uniformly on s to f.

Note this is not a tautology, since our definition of TendstoLocallyUniformlyOn is slightly more general (although the conditions are equivalent if β is locally compact and s is open, see tendstoLocallyUniformlyOn_TFAE).

@[deprecated tendstoLocallyUniformlyOn_of_forall_exists_nhds (since := "2025-05-22")]

theorem tendstoLocallyUniformlyOn_of_forall_exists_nhd {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, TendstoUniformlyOn F f p t) : TendstoLocallyUniformlyOn F f p s

Alias of tendstoLocallyUniformlyOn_of_forall_exists_nhds.

---

If every x ∈ s has a neighbourhood within s on which F i tends uniformly to f, then F i tends locally uniformly on s to f.

Note this is not a tautology, since our definition of TendstoLocallyUniformlyOn is slightly more general (although the conditions are equivalent if β is locally compact and s is open, see tendstoLocallyUniformlyOn_TFAE).

theorem tendstoLocallyUniformly_of_forall_exists_nhds {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : ∀ (x : α), ∃ t ∈ nhds x, TendstoUniformlyOn F f p t) : TendstoLocallyUniformly F f p

If every x has a neighbourhood on which F i tends uniformly to f, then F i tends locally uniformly to f. (Special case of tendstoLocallyUniformlyOn_of_forall_exists_nhds where s = univ.)

@[deprecated tendstoLocallyUniformly_of_forall_exists_nhds (since := "2025-05-22")]

theorem tendstoLocallyUniformly_of_forall_exists_nhd {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : ∀ (x : α), ∃ t ∈ nhds x, TendstoUniformlyOn F f p t) : TendstoLocallyUniformly F f p

Alias of tendstoLocallyUniformly_of_forall_exists_nhds.

---

If every x has a neighbourhood on which F i tends uniformly to f, then F i tends locally uniformly to f. (Special case of tendstoLocallyUniformlyOn_of_forall_exists_nhds where s = univ.)

theorem tendstoLocallyUniformlyOn_TFAE {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {s : Set α} [LocallyCompactSpace α] (G : ι → α → β) (g : α → β) (p : Filter ι) (hs : IsOpen s) : [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K, ∀ x ∈ s, ∃ v ∈ nhdsWithin x s, TendstoUniformlyOn G g p v].TFAE

theorem tendstoLocallyUniformlyOn_iff_forall_isCompact {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [LocallyCompactSpace α] (hs : IsOpen s) : TendstoLocallyUniformlyOn F f p s ↔ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn F f p K

theorem tendstoLocallyUniformly_iff_forall_isCompact {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [LocallyCompactSpace α] : TendstoLocallyUniformly F f p ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn F f p K

theorem tendstoLocallyUniformlyOn_iff_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (nhdsWithin x s)

theorem tendstoLocallyUniformly_iff_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (nhds x)

theorem TendstoLocallyUniformlyOn.tendsto_at {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (hf : TendstoLocallyUniformlyOn F f p s) {a : α} (ha : a ∈ s) : Filter.Tendsto (fun (i : ι) => F i a) p (nhds (f a))

theorem TendstoLocallyUniformlyOn.unique {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [p.NeBot] [T2Space β] {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : TendstoLocallyUniformlyOn F g p s) : Set.EqOn f g s

theorem TendstoLocallyUniformlyOn.congr {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {G : ι → α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : ∀ (n : ι), Set.EqOn (F n) (G n) s) : TendstoLocallyUniformlyOn G f p s

theorem TendstoLocallyUniformlyOn.congr_right {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : Set.EqOn f g s) : TendstoLocallyUniformlyOn F g p s