Uniform convergence

A sequence of functions Fₙ (with values in a metric space) converges uniformly on a set s to a function f if, for all ε > 0, for all large enough n, one has for all y ∈ s the inequality dist (f y, Fₙ y) < ε. Under uniform convergence, many properties of the Fₙ pass to the limit, most notably continuity. We prove this in the file, defining the notion of uniform convergence in the more general setting of uniform spaces, and with respect to an arbitrary indexing set endowed with a filter (instead of just ℕ with atTop).

Main results

Let α be a topological space, β a uniform space, Fₙ and f be functions from α to β (where the index n belongs to an indexing type ι endowed with a filter p).

• TendstoUniformlyOn F f p s: the fact that Fₙ converges uniformly to f on s. This means that, for any entourage u of the diagonal, for large enough n (with respect to p), one has (f y, Fₙ y) ∈ u for all y ∈ s.
• TendstoUniformly F f p: same notion with s = univ.
• TendstoUniformlyOn.continuousOn: a uniform limit on a set of functions which are continuous on this set is itself continuous on this set.
• TendstoUniformly.continuous: a uniform limit of continuous functions is continuous.
• TendstoUniformlyOn.tendsto_comp: 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.
• TendstoUniformly.tendsto_comp: If Fₙ tends uniformly to f, and gₙ tends to x, then Fₙ gₙ tends to f x.

Finally, we introduce the notion of a uniform Cauchy sequence, which is to uniform convergence what a Cauchy sequence is to the usual notion of convergence.

Implementation notes

We derive most of our initial results from an auxiliary definition TendstoUniformlyOnFilter. This definition in and of itself can sometimes be useful, e.g., when studying the local behavior of the Fₙ near a point, which would typically look like TendstoUniformlyOnFilter F f p (𝓝 x). Still, while this may be the "correct" definition (see tendstoUniformlyOn_iff_tendstoUniformlyOnFilter), it is somewhat unwieldy to work with in practice. Thus, we provide the more traditional definition in TendstoUniformlyOn.

Tags

Uniform limit, uniform convergence, tends uniformly to

Different notions of uniform convergence

We define uniform convergence, on a set or in the whole space.

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

A sequence of functions Fₙ converges uniformly on a filter p' to a limiting function f with respect to the filter p if, for any entourage of the diagonal u, one has p ×ˢ p'-eventually (f x, Fₙ x) ∈ u.

Equations

• TendstoUniformlyOnFilter F f p p' = ∀ u ∈ uniformity β, ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

theorem tendstoUniformlyOnFilter_iff_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} : TendstoUniformlyOnFilter F f p p' ↔ Filter.Tendsto (fun (q : ι × α) => (f q.2, F q.1 q.2)) (p ×ˢ p') (uniformity β)

A sequence of functions Fₙ converges uniformly on a filter p' to a limiting function f w.r.t. filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ˢ p' to the uniformity. In other words: one knows nothing about the behavior of x in this limit besides it being in p'.

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

A sequence of functions Fₙ converges uniformly on a set s to a limiting function f with respect to the filter p if, for any entourage of the diagonal u, one has p-eventually (f x, Fₙ x) ∈ u for all x ∈ s.

Equations

• TendstoUniformlyOn F f p s = ∀ u ∈ uniformity β, ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

theorem tendstoUniformlyOn_iff_tendstoUniformlyOnFilter {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (Filter.principal s)

theorem TendstoUniformlyOn.tendstoUniformlyOnFilter {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOn F f p s → TendstoUniformlyOnFilter F f p (Filter.principal s)

Alias of the forward direction of tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.

theorem TendstoUniformlyOnFilter.tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOnFilter F f p (Filter.principal s) → TendstoUniformlyOn F f p s

Alias of the reverse direction of tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.

theorem tendstoUniformlyOn_iff_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOn F f p s ↔ Filter.Tendsto (fun (q : ι × α) => (f q.2, F q.1 q.2)) (p ×ˢ Filter.principal s) (uniformity β)

A sequence of functions Fₙ converges uniformly on a set s to a limiting function f w.r.t. filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ˢ 𝓟 s to the uniformity. In other words: one knows nothing about the behavior of x in this limit besides it being in s.

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

A sequence of functions Fₙ converges uniformly to a limiting function f with respect to a filter p if, for any entourage of the diagonal u, one has p-eventually (f x, Fₙ x) ∈ u for all x.

Equations

• TendstoUniformly F f p = ∀ u ∈ uniformity β, ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ u

theorem tendstoUniformlyOn_univ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformlyOn F f p Set.univ ↔ TendstoUniformly F f p

theorem tendstoUniformly_iff_tendstoUniformlyOnFilter {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

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

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

theorem tendstoUniformly_iff_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformly F f p ↔ Filter.Tendsto (fun (q : ι × α) => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (uniformity β)

A sequence of functions Fₙ converges uniformly to a limiting function f w.r.t. filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ˢ ⊤ to the uniformity. In other words: one knows nothing about the behavior of x in this limit.

theorem TendstoUniformlyOnFilter.tendsto_at {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {p' : Filter α} (h : TendstoUniformlyOnFilter F f p p') (hx : Filter.principal {x} ≤ p') : Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))

Uniform convergence implies pointwise convergence.

theorem TendstoUniformlyOn.tendsto_at {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α} {p : Filter ι} (h : TendstoUniformlyOn F f p s) (hx : x ∈ s) : Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))

Uniform convergence implies pointwise convergence.

theorem TendstoUniformly.tendsto_at {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : TendstoUniformly F f p) (x : α) : Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))

Uniform convergence implies pointwise convergence.

theorem TendstoUniformlyOnFilter.mono_left {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {p'' : Filter ι} (h : TendstoUniformlyOnFilter F f p p') (hp : p'' ≤ p) : TendstoUniformlyOnFilter F f p'' p'

theorem TendstoUniformlyOnFilter.mono_right {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' p'' : Filter α} (h : TendstoUniformlyOnFilter F f p p') (hp : p'' ≤ p') : TendstoUniformlyOnFilter F f p p''

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

theorem TendstoUniformlyOnFilter.congr {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {F' : ι → α → β} (hf : TendstoUniformlyOnFilter F f p p') (hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2) : TendstoUniformlyOnFilter F' f p p'

theorem TendstoUniformlyOn.congr {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {F' : ι → α → β} (hf : TendstoUniformlyOn F f p s) (hff' : ∀ᶠ (n : ι) in p, Set.EqOn (F n) (F' n) s) : TendstoUniformlyOn F' f p s

theorem tendstoUniformly_congr {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {F' : ι → α → β} (hF : F =ᶠ[p] F') : TendstoUniformly F f p ↔ TendstoUniformly F' f p

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

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

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

Composing on the right by a function preserves uniform convergence on a filter

theorem TendstoUniformlyOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoUniformlyOn F f p s) (g : γ → α) : TendstoUniformlyOn (fun (n : ι) => F n ∘ g) (f ∘ g) p (g ⁻¹' s)

Composing on the right by a function preserves uniform convergence on a set

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

Composing on the right by a function preserves uniform convergence

theorem UniformContinuous.comp_tendstoUniformlyOnFilter {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformlyOnFilter F f p p') : TendstoUniformlyOnFilter (fun (i : ι) => g ∘ F i) (g ∘ f) p p'

Composing on the left by a uniformly continuous function preserves uniform convergence on a filter

theorem UniformContinuous.comp_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformlyOn F f p s) : TendstoUniformlyOn (fun (i : ι) => g ∘ F i) (g ∘ f) p s

Composing on the left by a uniformly continuous function preserves uniform convergence on a set

theorem UniformContinuous.comp_tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformly F f p) : TendstoUniformly (fun (i : ι) => g ∘ F i) (g ∘ f) p

Composing on the left by a uniformly continuous function preserves uniform convergence

theorem TendstoUniformlyOnFilter.prodMap {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {q : Filter ι'} {q' : Filter α'} (h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q q') : TendstoUniformlyOnFilter (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')

@[deprecated TendstoUniformlyOnFilter.prodMap (since := "2025-03-10")]

theorem TendstoUniformlyOnFilter.prod_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {q : Filter ι'} {q' : Filter α'} (h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q q') : TendstoUniformlyOnFilter (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')

Alias of TendstoUniformlyOnFilter.prodMap.

theorem TendstoUniformlyOn.prodMap {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'} {s' : Set α'} (h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s') : TendstoUniformlyOn (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')

@[deprecated TendstoUniformlyOn.prodMap (since := "2025-03-10")]

theorem TendstoUniformlyOn.prod_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'} {s' : Set α'} (h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s') : TendstoUniformlyOn (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')

Alias of TendstoUniformlyOn.prodMap.

theorem TendstoUniformly.prodMap {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') : TendstoUniformly (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')

@[deprecated TendstoUniformly.prodMap (since := "2025-03-10")]

theorem TendstoUniformly.prod_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') : TendstoUniformly (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')

Alias of TendstoUniformly.prodMap.

theorem TendstoUniformlyOnFilter.prodMk {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {ι' : Type u_5} {β' : Type u_6} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {q : Filter ι'} (h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q p') : TendstoUniformlyOnFilter (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p ×ˢ q) p'

@[deprecated TendstoUniformlyOnFilter.prodMk (since := "2025-03-10")]

theorem TendstoUniformlyOnFilter.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {ι' : Type u_5} {β' : Type u_6} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {q : Filter ι'} (h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q p') : TendstoUniformlyOnFilter (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p ×ˢ q) p'

Alias of TendstoUniformlyOnFilter.prodMk.

theorem TendstoUniformlyOn.prodMk {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {β' : Type u_6} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'} (h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s) : TendstoUniformlyOn (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p ×ˢ p') s

@[deprecated TendstoUniformlyOn.prodMk (since := "2025-03-10")]

theorem TendstoUniformlyOn.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {β' : Type u_6} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'} (h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s) : TendstoUniformlyOn (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p ×ˢ p') s

Alias of TendstoUniformlyOn.prodMk.

theorem TendstoUniformly.prodMk {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {ι' : Type u_5} {β' : Type u_6} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') : TendstoUniformly (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p ×ˢ p')

@[deprecated TendstoUniformly.prodMk (since := "2025-03-10")]

theorem TendstoUniformly.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {ι' : Type u_5} {β' : Type u_6} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') : TendstoUniformly (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p ×ˢ p')

Alias of TendstoUniformly.prodMk.

theorem tendsto_prod_filter_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α} {c : β} : Filter.Tendsto (↿F) (p ×ˢ p') (nhds c) ↔ TendstoUniformlyOnFilter F (fun (x : α) => c) p p'

Uniform convergence on a filter p' to a constant function is equivalent to convergence in p ×ˢ p'.

theorem tendsto_prod_principal_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {c : β} : Filter.Tendsto (↿F) (p ×ˢ Filter.principal s) (nhds c) ↔ TendstoUniformlyOn F (fun (x : α) => c) p s

Uniform convergence on a set s to a constant function is equivalent to convergence in p ×ˢ 𝓟 s.

theorem tendsto_prod_top_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {c : β} : Filter.Tendsto (↿F) (p ×ˢ ⊤) (nhds c) ↔ TendstoUniformly F (fun (x : α) => c) p

Uniform convergence to a constant function is equivalent to convergence in p ×ˢ ⊤.

theorem tendstoUniformlyOn_empty {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformlyOn F f p ∅

Uniform convergence on the empty set is vacuously true

theorem tendstoUniformlyOn_singleton_iff_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} : TendstoUniformlyOn F f p {x} ↔ Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))

Uniform convergence on a singleton is equivalent to regular convergence

theorem Filter.Tendsto.tendstoUniformlyOnFilter_const {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {p : Filter ι} {g : ι → β} {b : β} (hg : Tendsto g p (nhds b)) (p' : Filter α) : TendstoUniformlyOnFilter (fun (n : ι) (x : α) => g n) (fun (x : α) => b) p p'

If a sequence g converges to some b, then the sequence of constant functions fun n ↦ fun a ↦ g n converges to the constant function fun a ↦ b on any set s

theorem Filter.Tendsto.tendstoUniformlyOn_const {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {p : Filter ι} {g : ι → β} {b : β} (hg : Tendsto g p (nhds b)) (s : Set α) : TendstoUniformlyOn (fun (n : ι) (x : α) => g n) (fun (x : α) => b) p s

If a sequence g converges to some b, then the sequence of constant functions fun n ↦ fun a ↦ g n converges to the constant function fun a ↦ b on any set s

theorem UniformContinuousOn.tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {x : α} [UniformSpace α] [UniformSpace γ] {U : Set α} {V : Set β} {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ V)) (hU : x ∈ U) : TendstoUniformlyOn F (F x) (nhdsWithin x U) V

theorem UniformContinuousOn.tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {x : α} [UniformSpace α] [UniformSpace γ] {U : Set α} (hU : U ∈ nhds x) {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ Set.univ)) : TendstoUniformly F (F x) (nhds x)

theorem UniformContinuous₂.tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {x : α} [UniformSpace α] [UniformSpace γ] {f : α → β → γ} (h : UniformContinuous₂ f) : TendstoUniformly f (f x) (nhds x)

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

A sequence is uniformly Cauchy if eventually all of its pairwise differences are uniformly bounded

Equations

• UniformCauchySeqOnFilter F p p' = ∀ u ∈ uniformity β, ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

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

A sequence is uniformly Cauchy if eventually all of its pairwise differences are uniformly bounded

Equations

• UniformCauchySeqOn F p s = ∀ u ∈ uniformity β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

theorem uniformCauchySeqOn_iff_uniformCauchySeqOnFilter {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} : UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (Filter.principal s)

theorem UniformCauchySeqOn.uniformCauchySeqOnFilter {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} (hF : UniformCauchySeqOn F p s) : UniformCauchySeqOnFilter F p (Filter.principal s)

theorem TendstoUniformlyOnFilter.uniformCauchySeqOnFilter {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} (hF : TendstoUniformlyOnFilter F f p p') : UniformCauchySeqOnFilter F p p'

A sequence that converges uniformly is also uniformly Cauchy

theorem TendstoUniformlyOn.uniformCauchySeqOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (hF : TendstoUniformlyOn F f p s) : UniformCauchySeqOn F p s

A sequence that converges uniformly is also uniformly Cauchy

theorem UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} (hF : UniformCauchySeqOnFilter F p p') (hF' : ∀ᶠ (x : α) in p', Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))) : TendstoUniformlyOnFilter F f p p'

A uniformly Cauchy sequence converges uniformly to its limit

theorem UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (hF : UniformCauchySeqOn F p s) (hF' : ∀ x ∈ s, Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))) : TendstoUniformlyOn F f p s

A uniformly Cauchy sequence converges uniformly to its limit

theorem UniformCauchySeqOnFilter.mono_left {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α} {p'' : Filter ι} (hf : UniformCauchySeqOnFilter F p p') (hp : p'' ≤ p) : UniformCauchySeqOnFilter F p'' p'

theorem UniformCauchySeqOnFilter.mono_right {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' p'' : Filter α} (hf : UniformCauchySeqOnFilter F p p') (hp : p'' ≤ p') : UniformCauchySeqOnFilter F p p''

theorem UniformCauchySeqOn.mono {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s s' : Set α} {p : Filter ι} (hf : UniformCauchySeqOn F p s) (hss' : s' ⊆ s) : UniformCauchySeqOn F p s'

theorem UniformCauchySeqOnFilter.comp {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α} {γ : Type u_5} (hf : UniformCauchySeqOnFilter F p p') (g : γ → α) : UniformCauchySeqOnFilter (fun (n : ι) => F n ∘ g) p (Filter.comap g p')

Composing on the right by a function preserves uniform Cauchy sequences

theorem UniformCauchySeqOn.comp {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {γ : Type u_5} (hf : UniformCauchySeqOn F p s) (g : γ → α) : UniformCauchySeqOn (fun (n : ι) => F n ∘ g) p (g ⁻¹' s)

Composing on the right by a function preserves uniform Cauchy sequences

theorem UniformContinuous.comp_uniformCauchySeqOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (hf : UniformCauchySeqOn F p s) : UniformCauchySeqOn (fun (n : ι) => g ∘ F n) p s

Composing on the left by a uniformly continuous function preserves uniform Cauchy sequences

theorem UniformCauchySeqOn.prodMap {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {p' : Filter ι'} {s' : Set α'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s') : UniformCauchySeqOn (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')

@[deprecated UniformCauchySeqOn.prodMap (since := "2025-03-10")]

theorem UniformCauchySeqOn.prod_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {p' : Filter ι'} {s' : Set α'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s') : UniformCauchySeqOn (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')

Alias of UniformCauchySeqOn.prodMap.

theorem UniformCauchySeqOn.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {β' : Type u_6} [UniformSpace β'] {F' : ι' → α → β'} {p' : Filter ι'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s) : UniformCauchySeqOn (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (p ×ˢ p') s

theorem UniformCauchySeqOn.prod' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {β' : Type u_5} [UniformSpace β'] {F' : ι → α → β'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p s) : UniformCauchySeqOn (fun (i : ι) (a : α) => (F i a, F' i a)) p s

theorem UniformCauchySeqOn.cauchy_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {x : α} {p : Filter ι} [hp : p.NeBot] (hf : UniformCauchySeqOn F p s) (hx : x ∈ s) : Cauchy (Filter.map (fun (i : ι) => F i x) p)

If a sequence of functions is uniformly Cauchy on a set, then the values at each point form a Cauchy sequence.

theorem UniformCauchySeqOn.cauchySeq {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {x : α} [Nonempty ι] [SemilatticeSup ι] (hf : UniformCauchySeqOn F Filter.atTop s) (hx : x ∈ s) : CauchySeq fun (i : ι) => F i x

If a sequence of functions is uniformly Cauchy on a set, then the values at each point form a Cauchy sequence. See UniformCauchSeqOn.cauchy_map for the non-atTop case.

theorem tendstoUniformlyOn_of_seq_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {l : Filter ι} [l.IsCountablyGenerated] (h : ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun (n : ℕ) => F (u n)) f Filter.atTop s) : TendstoUniformlyOn F f l s

theorem TendstoUniformlyOn.seq_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {l : Filter ι} (h : TendstoUniformlyOn F f l s) (u : ℕ → ι) (hu : Filter.Tendsto u Filter.atTop l) : TendstoUniformlyOn (fun (n : ℕ) => F (u n)) f Filter.atTop s

theorem tendstoUniformlyOn_iff_seq_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {l : Filter ι} [l.IsCountablyGenerated] : TendstoUniformlyOn F f l s ↔ ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun (n : ℕ) => F (u n)) f Filter.atTop s

theorem tendstoUniformly_iff_seq_tendstoUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {l : Filter ι} [l.IsCountablyGenerated] : TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformly (fun (n : ℕ) => F (u n)) f Filter.atTop

theorem TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} [p.NeBot] {L : ι → β} {ℓ : β} (h1 : TendstoUniformlyOnFilter F f p p') (h2 : ∀ᶠ (i : ι) in p, Filter.Tendsto (F i) p' (nhds (L i))) (h3 : Filter.Tendsto L p (nhds ℓ)) : Filter.Tendsto f p' (nhds ℓ)

theorem TendstoUniformly.tendsto_of_eventually_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} [p.NeBot] {L : ι → β} {ℓ : β} (h1 : TendstoUniformly F f p) (h2 : ∀ᶠ (i : ι) in p, Filter.Tendsto (F i) p' (nhds (L i))) (h3 : Filter.Tendsto L p (nhds ℓ)) : Filter.Tendsto f p' (nhds ℓ)