Mathlib.Topology.UniformSpace.UniformConvergence

TendstoUniformlyOnFilter definition

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

Full source

/-- 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`. -/
def TendstoUniformlyOnFilter (F : ι → α → β) (f : α → β) (p : Filter ι) (p' : Filter α) :=
  ∀ u ∈ 𝓤 β, ∀ᶠ n : ι × α in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u

Uniform convergence on a filter

Informal description

A family of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly on a filter $ p' $ to a limiting function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if, for any entourage $ u $ of the diagonal in the uniform space $ \beta $, the set of pairs $ (n, x) \in \iota \times \alpha $ such that $ (f(x), F_n(x)) \in u $ is eventually in the product filter $ p \times p' $.

tendstoUniformlyOnFilter_iff_tendsto theorem

: TendstoUniformlyOnFilter F f p p' ↔ Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)

Full source

/--
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'`.
-/
theorem tendstoUniformlyOnFilter_iff_tendsto :
    TendstoUniformlyOnFilterTendstoUniformlyOnFilter F f p p' ↔
      Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β) :=
  Iff.rfl

Characterization of Uniform Convergence on a Filter via Tendsto Condition

Informal description

A family of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly on a filter $ p' $ to a limiting function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if and only if the function $ (n, x) \mapsto (f(x), F_n(x)) $ converges to the uniformity filter $ \mathfrak{U}(\beta) $ along the product filter $ p \times p' $.

TendstoUniformlyOn definition

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

Full source

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

Uniform convergence on a set

Informal description

A family of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly on a set $ s \subseteq \alpha $ to a limiting function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if, for any entourage $ u $ of the diagonal in the uniform space $ \beta $, there exists an event in $ p $ such that for all $ n $ in this event and all $ x \in s $, the pair $ (f(x), F_n(x)) $ belongs to $ u $.

tendstoUniformlyOn_iff_tendstoUniformlyOnFilter theorem

: TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (𝓟 s)

Full source

theorem tendstoUniformlyOn_iff_tendstoUniformlyOnFilter :
    TendstoUniformlyOnTendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (𝓟 s) := by
  simp only [TendstoUniformlyOn, TendstoUniformlyOnFilter]
  apply forall₂_congr
  simp_rw [eventually_prod_principal_iff]
  simp

Equivalence of Uniform Convergence on a Set and on its Principal Filter

Informal description

A family of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly on a set $ s \subseteq \alpha $ to a limiting function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if and only if $ F_n $ converges uniformly to $ f $ on the principal filter generated by $ s $.

tendstoUniformlyOn_iff_tendsto theorem

: TendstoUniformlyOn F f p s ↔ Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)

Full source

/-- 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`.
-/
theorem tendstoUniformlyOn_iff_tendsto :
    TendstoUniformlyOnTendstoUniformlyOn F f p s ↔
    Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β) := by
  simp [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

Characterization of Uniform Convergence on a Set via Product Filter Convergence

Informal description

A family of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly on a set $ s \subseteq \alpha $ to a limiting function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if and only if the function $ (n, x) \mapsto (f(x), F_n(x)) $ converges to the uniformity filter $ \mathfrak{U}(\beta) $ along the product filter $ p \times \mathfrak{P}(s) $, where $ \mathfrak{P}(s) $ is the principal filter generated by $ s $.

TendstoUniformly definition

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

Full source

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

Uniform convergence of a sequence of functions

Informal description

A sequence of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly to a function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if, for every entourage $ u $ of the diagonal in the uniform space $ \beta $, there exists an event $ N \in p $ such that for all $ n \in N $ and all $ x \in \alpha $, the pair $ (f(x), F_n(x)) $ belongs to $ u $.

tendstoUniformlyOn_univ theorem

: TendstoUniformlyOn F f p univ ↔ TendstoUniformly F f p

Full source

theorem tendstoUniformlyOn_univ : TendstoUniformlyOnTendstoUniformlyOn F f p univ ↔ TendstoUniformly F f p := by
  simp [TendstoUniformlyOn, TendstoUniformly]

Uniform Convergence on Universal Set is Equivalent to Uniform Convergence

Informal description

A family of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly on the universal set $ \text{univ} $ to a limiting function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if and only if $ F_n $ converges uniformly to $ f $ with respect to $ p $.

tendstoUniformly_iff_tendstoUniformlyOnFilter theorem

: TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

Full source

theorem tendstoUniformly_iff_tendstoUniformlyOnFilter :
    TendstoUniformlyTendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤ := by
  rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]

Equivalence of Uniform Convergence and Uniform Convergence on Trivial Filter

Informal description

A family of functions $F_n \colon \alpha \to \beta$ indexed by $n \in \iota$ converges uniformly to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$ if and only if $F_n$ converges uniformly to $f$ on the trivial filter $\top$ (i.e., the filter containing all subsets of $\alpha$).

TendstoUniformly.tendstoUniformlyOnFilter theorem

(h : TendstoUniformly F f p) : TendstoUniformlyOnFilter F f p ⊤

Full source

theorem TendstoUniformly.tendstoUniformlyOnFilter (h : TendstoUniformly F f p) :
    TendstoUniformlyOnFilter F f p ⊤ := by rwa [← tendstoUniformly_iff_tendstoUniformlyOnFilter]

Uniform convergence implies uniform convergence on trivial filter

Informal description

If a family 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 $ \iota $, then $ F_n $ converges uniformly to $ f $ on the trivial filter $ \top $ (i.e., the filter containing all subsets of $ \alpha $).

tendstoUniformlyOn_iff_tendstoUniformly_comp_coe theorem

: TendstoUniformlyOn F f p s ↔ TendstoUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p

Full source

theorem tendstoUniformlyOn_iff_tendstoUniformly_comp_coe :
    TendstoUniformlyOnTendstoUniformlyOn F f p s ↔ TendstoUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p :=
  forall₂_congr fun u _ => by simp

Uniform Convergence on Set is Equivalent to Uniform Convergence of Restrictions

Informal description

A family of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly on a set $ s \subseteq \alpha $ to a function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if and only if the restricted family $ F_n \restriction s $ converges uniformly to $ f \restriction s $ on the entire space $ s $.

tendstoUniformly_iff_tendsto theorem

: TendstoUniformly F f p ↔ Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (𝓤 β)

Full source

/-- 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 tendstoUniformly_iff_tendsto :
    TendstoUniformlyTendstoUniformly F f p ↔ Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (𝓤 β) := by
  simp [tendstoUniformly_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

Uniform Convergence Criterion via Product Filter

Informal description

A family of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ converges uniformly to a function $ f : \alpha \to \beta $ with respect to a filter $ p $ on $ \iota $ if and only if the function $ (n, x) \mapsto (f(x), F_n(x)) $ converges to the uniformity of $ \beta $ along the product filter $ p \times \top $.

TendstoUniformlyOnFilter.tendsto_at theorem

(h : TendstoUniformlyOnFilter F f p p') (hx : 𝓟 { x } ≤ p') : Tendsto (fun n => F n x) p <| 𝓝 (f x)

Full source

/-- Uniform convergence implies pointwise convergence. -/
theorem TendstoUniformlyOnFilter.tendsto_at (h : TendstoUniformlyOnFilter F f p p')
    (hx : 𝓟 {x} ≤ p') : Tendsto (fun n => F n x) p <| 𝓝 (f x) := by
  refine Uniform.tendsto_nhds_right.mpr fun u hu => mem_map.mpr ?_
  filter_upwards [(h u hu).curry]
  intro i h
  simpa using h.filter_mono hx

Pointwise convergence under uniform convergence on a filter

Informal description

Let $F_n : \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ converging uniformly on a filter $p'$ to a function $f : \alpha \to \beta$ with respect to a filter $p$ on $\iota$. If the principal filter at a point $x \in \alpha$ is contained in $p'$, then $F_n(x)$ converges to $f(x)$ with respect to $p$.

TendstoUniformlyOn.tendsto_at theorem

(h : TendstoUniformlyOn F f p s) (hx : x ∈ s) : Tendsto (fun n => F n x) p <| 𝓝 (f x)

Full source

/-- Uniform convergence implies pointwise convergence. -/
theorem TendstoUniformlyOn.tendsto_at (h : TendstoUniformlyOn F f p s) (hx : x ∈ s) :
    Tendsto (fun n => F n x) p <| 𝓝 (f x) :=
  h.tendstoUniformlyOnFilter.tendsto_at
    (le_principal_iff.mpr <| mem_principal.mpr <| singleton_subset_iff.mpr <| hx)

Uniform convergence implies pointwise convergence on a set

Informal description

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

TendstoUniformly.tendsto_at theorem

(h : TendstoUniformly F f p) (x : α) : Tendsto (fun n => F n x) p <| 𝓝 (f x)

Full source

/-- Uniform convergence implies pointwise convergence. -/
theorem TendstoUniformly.tendsto_at (h : TendstoUniformly F f p) (x : α) :
    Tendsto (fun n => F n x) p <| 𝓝 (f x) :=
  h.tendstoUniformlyOnFilter.tendsto_at le_top

Uniform convergence implies pointwise convergence

Informal description

Let $F_n \colon \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ that converges uniformly to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. Then for any point $x \in \alpha$, the sequence $F_n(x)$ converges to $f(x)$ with respect to $p$.

TendstoUniformlyOnFilter.mono_left theorem

{p'' : Filter ι} (h : TendstoUniformlyOnFilter F f p p') (hp : p'' ≤ p) : TendstoUniformlyOnFilter F f p'' p'

Full source

theorem TendstoUniformlyOnFilter.mono_left {p'' : Filter ι} (h : TendstoUniformlyOnFilter F f p p')
    (hp : p'' ≤ p) : TendstoUniformlyOnFilter F f p'' p' := fun u hu =>
  (h u hu).filter_mono (p'.prod_mono_left hp)

Uniform convergence is preserved under refinement of the index filter

Informal description

Let $F_n : \alpha \to \beta$ be a family of functions indexed by $n \in \iota$, converging uniformly on a filter $p'$ to a function $f : \alpha \to \beta$ with respect to a filter $p$ on $\iota$. If $p''$ is another filter on $\iota$ such that $p'' \leq p$, then $F_n$ converges uniformly to $f$ on $p'$ with respect to $p''$.

TendstoUniformlyOnFilter.mono_right theorem

{p'' : Filter α} (h : TendstoUniformlyOnFilter F f p p') (hp : p'' ≤ p') : TendstoUniformlyOnFilter F f p p''

Full source

theorem TendstoUniformlyOnFilter.mono_right {p'' : Filter α} (h : TendstoUniformlyOnFilter F f p p')
    (hp : p'' ≤ p') : TendstoUniformlyOnFilter F f p p'' := fun u hu =>
  (h u hu).filter_mono (p.prod_mono_right hp)

Uniform convergence is preserved under filter refinement

Informal description

Let $F_n : \alpha \to \beta$ be a family of functions indexed by $n \in \iota$, converging uniformly on a filter $p'$ to a function $f : \alpha \to \beta$ with respect to a filter $p$ on $\iota$. If $p''$ is another filter on $\alpha$ such that $p'' \leq p'$, then $F_n$ converges uniformly to $f$ on $p''$ with respect to $p$.

TendstoUniformlyOn.mono theorem

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

Full source

theorem TendstoUniformlyOn.mono (h : TendstoUniformlyOn F f p s) (h' : s' ⊆ s) :
    TendstoUniformlyOn F f p s' :=
  tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr
    (h.tendstoUniformlyOnFilter.mono_right (le_principal_iff.mpr <| mem_principal.mpr h'))

Uniform Convergence is Preserved Under Subset Restriction

Informal description

Let $F_n \colon \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ that converges uniformly to $f \colon \alpha \to \beta$ on a set $s \subseteq \alpha$ with respect to a filter $p$ on $\iota$. If $s'$ is a subset of $s$, then $F_n$ also converges uniformly to $f$ on $s'$ with respect to $p$.

TendstoUniformlyOnFilter.congr theorem

 {F' : ι → α → β} (hf : TendstoUniformlyOnFilter F f p p')
  (hff' : ∀ᶠ n : ι × α in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd) : TendstoUniformlyOnFilter F' f p p'

Full source

theorem TendstoUniformlyOnFilter.congr {F' : ι → α → β} (hf : TendstoUniformlyOnFilter F f p p')
    (hff' : ∀ᶠ n : ι × α in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd) :
    TendstoUniformlyOnFilter F' f p p' := by
  refine fun u hu => ((hf u hu).and hff').mono fun n h => ?_
  rw [← h.right]
  exact h.left

Uniform convergence is preserved under pointwise equality on a filter

Informal description

Let $F_n \colon \alpha \to \beta$ and $F'_n \colon \alpha \to \beta$ be two families of functions indexed by $n \in \iota$, and let $f \colon \alpha \to \beta$ be a limiting function. Suppose $F_n$ converges uniformly to $f$ on a filter $p'$ with respect to a filter $p$ on $\iota$. If for all $(n, x)$ in a set that is eventually in the product filter $p \times p'$, we have $F_n(x) = F'_n(x)$, then $F'_n$ also converges uniformly to $f$ on $p'$ with respect to $p$.

TendstoUniformlyOn.congr theorem

 {F' : ι → α → β} (hf : TendstoUniformlyOn F f p s) (hff' : ∀ᶠ n in p, Set.EqOn (F n) (F' n) s) :
  TendstoUniformlyOn F' f p s

Full source

theorem TendstoUniformlyOn.congr {F' : ι → α → β} (hf : TendstoUniformlyOn F f p s)
    (hff' : ∀ᶠ n in p, Set.EqOn (F n) (F' n) s) : TendstoUniformlyOn F' f p s := by
  rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at hf ⊢
  refine hf.congr ?_
  rw [eventually_iff] at hff' ⊢
  simp only [Set.EqOn] at hff'
  simp only [mem_prod_principal, hff', mem_setOf_eq]

Uniform Convergence is Preserved Under Pointwise Equality on a Set

Informal description

Let $F_n, F'_n \colon \alpha \to \beta$ be two families of functions indexed by $n \in \iota$, and let $f \colon \alpha \to \beta$ be a limiting function. Suppose $F_n$ converges uniformly to $f$ on a set $s \subseteq \alpha$ with respect to a filter $p$ on $\iota$. If for all $n$ in some event in $p$, the functions $F_n$ and $F'_n$ are equal on $s$, then $F'_n$ also converges uniformly to $f$ on $s$ with respect to $p$.

tendstoUniformly_congr theorem

{F' : ι → α → β} (hF : F =ᶠ[p] F') : TendstoUniformly F f p ↔ TendstoUniformly F' f p

Full source

lemma tendstoUniformly_congr {F' : ι → α → β} (hF : F =ᶠ[p] F') :
    TendstoUniformlyTendstoUniformly F f p ↔ TendstoUniformly F' f p := by
  simp_rw [← tendstoUniformlyOn_univ] at *
  have HF := EventuallyEq.exists_mem hF
  exact ⟨fun h => h.congr (by aesop), fun h => h.congr (by simp_rw [eqOn_comm]; aesop)⟩

Uniform Convergence is Equivalent Under Eventual Pointwise Equality

Informal description

Let $F_n, F'_n \colon \alpha \to \beta$ be two families of functions indexed by $n \in \iota$, and let $f \colon \alpha \to \beta$ be a function. If $F_n$ and $F'_n$ are eventually equal with respect to a filter $p$ on $\iota$ (i.e., $F_n = F'_n$ for all $n$ in some event in $p$), then $F_n$ converges uniformly to $f$ with respect to $p$ if and only if $F'_n$ converges uniformly to $f$ with respect to $p$.

TendstoUniformlyOn.congr_right theorem

{g : α → β} (hf : TendstoUniformlyOn F f p s) (hfg : EqOn f g s) : TendstoUniformlyOn F g p s

Full source

theorem TendstoUniformlyOn.congr_right {g : α → β} (hf : TendstoUniformlyOn F f p s)
    (hfg : EqOn f g s) : TendstoUniformlyOn F g p s := fun u hu => by
  filter_upwards [hf u hu] with i hi a ha using hfg ha ▸ hi a ha

Uniform limit is preserved under pointwise equality on the domain

Informal description

Let $F_n \colon \alpha \to \beta$ be a sequence of functions indexed by $n \in \iota$ and converging uniformly on a set $s \subseteq \alpha$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. If $g \colon \alpha \to \beta$ is another function that coincides with $f$ on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then $F_n$ also converges uniformly to $g$ on $s$ with respect to $p$.

TendstoUniformly.tendstoUniformlyOn theorem

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

Full source

protected theorem TendstoUniformly.tendstoUniformlyOn (h : TendstoUniformly F f p) :
    TendstoUniformlyOn F f p s :=
  (tendstoUniformlyOn_univ.2 h).mono (subset_univ s)

Uniform convergence implies uniform convergence on any subset

Informal description

If a family of functions $F_n \colon \alpha \to \beta$ indexed by $n \in \iota$ converges uniformly to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$, then for any subset $s \subseteq \alpha$, the family $F_n$ also converges uniformly to $f$ on $s$ with respect to $p$.

TendstoUniformlyOnFilter.comp theorem

 (h : TendstoUniformlyOnFilter F f p p') (g : γ → α) :
  TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (p'.comap g)

Full source

/-- Composing on the right by a function preserves uniform convergence on a filter -/
theorem TendstoUniformlyOnFilter.comp (h : TendstoUniformlyOnFilter F f p p') (g : γ → α) :
    TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (p'.comap g) := by
  rw [tendstoUniformlyOnFilter_iff_tendsto] at h ⊢
  exact h.comp (tendsto_id.prodMap tendsto_comap)

Uniform Convergence is Preserved Under Right Composition

Informal description

Let $F_n \colon \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ that converges uniformly on a filter $p'$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. For any function $g \colon \gamma \to \alpha$, the composed family $F_n \circ g \colon \gamma \to \beta$ converges uniformly on the pullback filter $p'.comap(g)$ to $f \circ g \colon \gamma \to \beta$ with respect to the same filter $p$.

TendstoUniformlyOn.comp theorem

(h : TendstoUniformlyOn F f p s) (g : γ → α) : TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s)

Full source

/-- Composing on the right by a function preserves uniform convergence on a set -/
theorem TendstoUniformlyOn.comp (h : TendstoUniformlyOn F f p s) (g : γ → α) :
    TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s) := by
  rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h ⊢
  simpa [TendstoUniformlyOn, comap_principal] using TendstoUniformlyOnFilter.comp h g

Uniform Convergence is Preserved Under Right Composition on a Set

Informal description

Let $F_n \colon \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ that converges uniformly on a set $s \subseteq \alpha$ to a function $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. For any function $g \colon \gamma \to \alpha$, the composed family $F_n \circ g \colon \gamma \to \beta$ converges uniformly on the preimage $g^{-1}(s)$ to $f \circ g \colon \gamma \to \beta$ with respect to the same filter $p$.

TendstoUniformly.comp theorem

(h : TendstoUniformly F f p) (g : γ → α) : TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p

Full source

/-- Composing on the right by a function preserves uniform convergence -/
theorem TendstoUniformly.comp (h : TendstoUniformly F f p) (g : γ → α) :
    TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p := by
  rw [tendstoUniformly_iff_tendstoUniformlyOnFilter] at h ⊢
  simpa [principal_univ, comap_principal] using h.comp g

Uniform Convergence is Preserved Under Right Composition

Informal description

Let $F_n \colon \alpha \to \beta$ be a sequence of functions indexed by $n \in \iota$ that converges uniformly to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. For any function $g \colon \gamma \to \alpha$, the composed sequence $F_n \circ g \colon \gamma \to \beta$ converges uniformly to $f \circ g \colon \gamma \to \beta$ with respect to the same filter $p$.

UniformContinuous.comp_tendstoUniformlyOnFilter theorem

 [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformlyOnFilter F f p p') :
  TendstoUniformlyOnFilter (fun i => g ∘ F i) (g ∘ f) p p'

Full source

/-- Composing on the left by a uniformly continuous function preserves
  uniform convergence on a filter -/
theorem UniformContinuous.comp_tendstoUniformlyOnFilter [UniformSpace γ] {g : β → γ}
    (hg : UniformContinuous g) (h : TendstoUniformlyOnFilter F f p p') :
    TendstoUniformlyOnFilter (fun i => g ∘ F i) (g ∘ f) p p' := fun _u hu => h _ (hg hu)

Uniform continuity preserves uniform convergence on a filter under composition

Informal description

Let $\alpha$ be a topological space, $\beta$ and $\gamma$ be uniform spaces, and $F_n \colon \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ converging uniformly on a filter $p'$ to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. If $g \colon \beta \to \gamma$ is a uniformly continuous function, then the family of compositions $g \circ F_n$ converges uniformly on $p'$ to $g \circ f$ with respect to $p$.

UniformContinuous.comp_tendstoUniformlyOn theorem

 [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformlyOn F f p s) :
  TendstoUniformlyOn (fun i => g ∘ F i) (g ∘ f) p s

Full source

/-- Composing on the left by a uniformly continuous function preserves
  uniform convergence on a set -/
theorem UniformContinuous.comp_tendstoUniformlyOn [UniformSpace γ] {g : β → γ}
    (hg : UniformContinuous g) (h : TendstoUniformlyOn F f p s) :
    TendstoUniformlyOn (fun i => g ∘ F i) (g ∘ f) p s := fun _u hu => h _ (hg hu)

Uniform continuity preserves uniform convergence on a set under composition

Informal description

Let $\alpha$ be a topological space, $\beta$ and $\gamma$ be uniform spaces, and $F_n \colon \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ converging uniformly on a set $s \subseteq \alpha$ to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. If $g \colon \beta \to \gamma$ is a uniformly continuous function, then the family of compositions $g \circ F_n$ converges uniformly on $s$ to $g \circ f$ with respect to $p$.

UniformContinuous.comp_tendstoUniformly theorem

 [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformly F f p) :
  TendstoUniformly (fun i => g ∘ F i) (g ∘ f) p

Full source

/-- Composing on the left by a uniformly continuous function preserves uniform convergence -/
theorem UniformContinuous.comp_tendstoUniformly [UniformSpace γ] {g : β → γ}
    (hg : UniformContinuous g) (h : TendstoUniformly F f p) :
    TendstoUniformly (fun i => g ∘ F i) (g ∘ f) p := fun _u hu => h _ (hg hu)

Uniform continuity preserves uniform convergence under composition

Informal description

Let $\alpha$ be a topological space, $\beta$ and $\gamma$ be uniform spaces, and $F_n \colon \alpha \to \beta$ be a sequence of functions indexed by $n \in \iota$ converging uniformly to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. If $g \colon \beta \to \gamma$ is a uniformly continuous function, then the sequence of compositions $g \circ F_n$ converges uniformly to $g \circ f$ with respect to the same filter $p$.

TendstoUniformlyOnFilter.prodMap theorem

 {ι' α' β' : Type*} [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')

Full source

theorem TendstoUniformlyOnFilter.prodMap {ι' α' β' : Type*} [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') := by
  rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢
  rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff, ← map_swap4_prod, tendsto_map'_iff]
  simpa using h.prodMap h'

Uniform Convergence of Product Functions on Product Filters

Informal description

Let $\alpha, \alpha'$ be topological spaces and $\beta, \beta'$ be uniform spaces. Given two families of functions $F_n \colon \alpha \to \beta$ and $F'_m \colon \alpha' \to \beta'$ indexed by $n \in \iota$ and $m \in \iota'$ respectively, suppose $F_n$ converges uniformly on a filter $p'$ to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$, and $F'_m$ converges uniformly on a filter $q'$ to $f' \colon \alpha' \to \beta'$ with respect to a filter $q$ on $\iota'$. Then the product family $(F_n \times F'_m) \colon \alpha \times \alpha' \to \beta \times \beta'$ converges uniformly on the product filter $p' \times q'$ to $f \times f'$ with respect to the product filter $p \times q$.

TendstoUniformlyOn.prodMap theorem

 {ι' α' β' : Type*} [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')

Full source

theorem TendstoUniformlyOn.prodMap {ι' α' β' : Type*} [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') := by
  rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h h' ⊢
  simpa only [prod_principal_principal] using h.prodMap h'

Uniform Convergence of Product Functions on Product Sets

Informal description

Let $\alpha, \alpha'$ be topological spaces and $\beta, \beta'$ be uniform spaces. Given two families of functions $F_n \colon \alpha \to \beta$ and $F'_m \colon \alpha' \to \beta'$ indexed by $n \in \iota$ and $m \in \iota'$ respectively, suppose $F_n$ converges uniformly on a set $s \subseteq \alpha$ to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$, and $F'_m$ converges uniformly on a set $s' \subseteq \alpha'$ to $f' \colon \alpha' \to \beta'$ with respect to a filter $p'$ on $\iota'$. Then the product family $(F_n \times F'_m) \colon \alpha \times \alpha' \to \beta \times \beta'$ converges uniformly on the product set $s \times s'$ to $f \times f'$ with respect to the product filter $p \times p'$.

TendstoUniformly.prodMap theorem

 {ι' α' β' : Type*} [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')

Full source

theorem TendstoUniformly.prodMap {ι' α' β' : Type*} [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') := by
  rw [← tendstoUniformlyOn_univ, ← univ_prod_univ] at *
  exact h.prodMap h'

Uniform Convergence of Product Functions under Product Filter

Informal description

Let $\alpha, \alpha'$ be topological spaces and $\beta, \beta'$ be uniform spaces. Given two families of functions $F_n \colon \alpha \to \beta$ and $F'_m \colon \alpha' \to \beta'$ indexed by $n \in \iota$ and $m \in \iota'$ respectively, suppose $F_n$ converges uniformly to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$, and $F'_m$ converges uniformly to $f' \colon \alpha' \to \beta'$ with respect to a filter $p'$ on $\iota'$. Then the product family $(F_n \times F'_m) \colon \alpha \times \alpha' \to \beta \times \beta'$ converges uniformly to $f \times f'$ with respect to the product filter $p \times p'$.

TendstoUniformlyOnFilter.prodMk theorem

 {ι' β' : Type*} [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'

Full source

theorem TendstoUniformlyOnFilter.prodMk {ι' β' : Type*} [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' :=
  fun u hu => ((h.prodMap h') u hu).diag_of_prod_right

Uniform Convergence of Paired Functions on a Common Filter

Informal description

Let $\alpha$ be a topological space and $\beta, \beta'$ be uniform spaces. Given two families of functions $F_n \colon \alpha \to \beta$ and $F'_m \colon \alpha \to \beta'$ indexed by $n \in \iota$ and $m \in \iota'$ respectively, suppose $F_n$ converges uniformly on a filter $p'$ to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$, and $F'_m$ converges uniformly on the same filter $p'$ to $f' \colon \alpha \to \beta'$ with respect to a filter $q$ on $\iota'$. Then the product family $(F_n, F'_m) \colon \alpha \to \beta \times \beta'$ converges uniformly on $p'$ to $(f, f')$ with respect to the product filter $p \times q$.

TendstoUniformlyOn.prodMk theorem

 {ι' β' : Type*} [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

Full source

protected theorem TendstoUniformlyOn.prodMk {ι' β' : Type*} [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 :=
  (congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a))

Uniform Convergence of Paired Functions on a Common Set

Informal description

Let $\alpha$ be a topological space and $\beta, \beta'$ be uniform spaces. Given two families of functions $F_n \colon \alpha \to \beta$ and $F'_m \colon \alpha \to \beta'$ indexed by $n \in \iota$ and $m \in \iota'$ respectively, suppose $F_n$ converges uniformly on a set $s \subseteq \alpha$ to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$, and $F'_m$ converges uniformly on the same set $s$ to $f' \colon \alpha \to \beta'$ with respect to a filter $p'$ on $\iota'$. Then the paired family $(F_n, F'_m) \colon \alpha \to \beta \times \beta'$ defined by $(F_n(x), F'_m(x))$ converges uniformly on $s$ to $(f(x), f'(x))$ with respect to the product filter $p \times p'$.

TendstoUniformly.prodMk theorem

 {ι' β' : Type*} [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')

Full source

theorem TendstoUniformly.prodMk {ι' β' : Type*} [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') :=
  (h.prodMap h').comp fun a => (a, a)

Uniform Convergence of Product Functions under Product Filter

Informal description

Let $\alpha$ be a topological space and $\beta, \beta'$ be uniform spaces. Given two families of functions $F_n \colon \alpha \to \beta$ and $F'_m \colon \alpha \to \beta'$ indexed by $n \in \iota$ and $m \in \iota'$ respectively, suppose $F_n$ converges uniformly to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$, and $F'_m$ converges uniformly to $f' \colon \alpha \to \beta'$ with respect to a filter $p'$ on $\iota'$. Then the product family $(F_n, F'_m) \colon \alpha \to \beta \times \beta'$ defined by $(F_n(x), F'_m(x))$ converges uniformly to $(f(x), f'(x))$ with respect to the product filter $p \times p'$.

tendsto_prod_filter_iff theorem

{c : β} : Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun _ => c) p p'

Full source

/-- Uniform convergence on a filter `p'` to a constant function is equivalent to convergence in
`p ×ˢ p'`. -/
theorem tendsto_prod_filter_iff {c : β} :
    TendstoTendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun _ => c) p p' := by
  simp_rw [nhds_eq_comap_uniformity, tendsto_comap_iff]
  rfl

Uniform Convergence to Constant Function vs. Pointwise Convergence in Product Filter

Informal description

For a family of functions $F_n : \alpha \to \beta$ indexed by $n \in \iota$ and a constant function $f(x) = c$ for some $c \in \beta$, the following are equivalent: 1. The uncurried function $(n, x) \mapsto F_n(x)$ tends to $c$ in the neighborhood filter as $(n, x)$ varies in the product filter $p \times p'$. 2. The family $F_n$ converges uniformly on the filter $p'$ to the constant function $f(x) = c$ with respect to the filter $p$ on $\iota$.

tendsto_prod_principal_iff theorem

{c : β} : Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun _ => c) p s

Full source

/-- Uniform convergence on a set `s` to a constant function is equivalent to convergence in
`p ×ˢ 𝓟 s`. -/
theorem tendsto_prod_principal_iff {c : β} :
    TendstoTendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun _ => c) p s := by
  rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]
  exact tendsto_prod_filter_iff

Uniform Convergence to Constant Function on Set vs. Pointwise Convergence in Product Filter with Principal Filter

Informal description

For a family of functions $F_n \colon \alpha \to \beta$ indexed by $n \in \iota$, a constant function $f(x) = c$ where $c \in \beta$, a filter $p$ on $\iota$, and a set $s \subseteq \alpha$, the following are equivalent: 1. The uncurried function $(n, x) \mapsto F_n(x)$ tends to $c$ in the neighborhood filter as $(n, x)$ varies in the product filter $p \times \mathcal{P}(s)$ (where $\mathcal{P}(s)$ is the principal filter generated by $s$). 2. The family $F_n$ converges uniformly on $s$ to the constant function $f(x) = c$ with respect to the filter $p$.

tendsto_prod_top_iff theorem

{c : β} : Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformly F (fun _ => c) p

Full source

/-- Uniform convergence to a constant function is equivalent to convergence in `p ×ˢ ⊤`. -/
theorem tendsto_prod_top_iff {c : β} :
    TendstoTendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformly F (fun _ => c) p := by
  rw [tendstoUniformly_iff_tendstoUniformlyOnFilter]
  exact tendsto_prod_filter_iff

Uniform Convergence to Constant Function vs. Pointwise Convergence in Full Space

Informal description

For a family of functions $F_n \colon \alpha \to \beta$ indexed by $n \in \iota$ and a constant function $f(x) = c$ where $c \in \beta$, the following are equivalent: 1. The uncurried function $(n, x) \mapsto F_n(x)$ tends to $c$ in the neighborhood filter as $(n, x)$ varies in the product filter $p \times \top$ (where $\top$ is the trivial filter on $\alpha$). 2. The family $F_n$ converges uniformly to the constant function $f(x) = c$ with respect to the filter $p$ on $\iota$.

tendstoUniformlyOn_empty theorem

: TendstoUniformlyOn F f p ∅

Full source

/-- Uniform convergence on the empty set is vacuously true -/
theorem tendstoUniformlyOn_empty : TendstoUniformlyOn F f p ∅ := fun u _ => by simp

Uniform Convergence on the Empty Set is Vacuously True

Informal description

For any family of functions $F_n \colon \alpha \to \beta$ indexed by $n \in \iota$, any limiting function $f \colon \alpha \to \beta$, and any filter $p$ on $\iota$, the sequence $F_n$ converges uniformly to $f$ on the empty set $\emptyset \subseteq \alpha$.

tendstoUniformlyOn_singleton_iff_tendsto theorem

: TendstoUniformlyOn F f p { x } ↔ Tendsto (fun n : ι => F n x) p (𝓝 (f x))

Full source

/-- Uniform convergence on a singleton is equivalent to regular convergence -/
theorem tendstoUniformlyOn_singleton_iff_tendsto :
    TendstoUniformlyOnTendstoUniformlyOn F f p {x} ↔ Tendsto (fun n : ι => F n x) p (𝓝 (f x)) := by
  simp_rw [tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right, tendsto_def]
  exact forall₂_congr fun u _ => by simp [mem_prod_principal, preimage]

Uniform Convergence on Singleton is Equivalent to Pointwise Convergence

Informal description

For a family of functions $F_n \colon \alpha \to \beta$ indexed by $n \in \iota$, a limiting function $f \colon \alpha \to \beta$, a filter $p$ on $\iota$, and a point $x \in \alpha$, the following are equivalent: 1. $F_n$ converges uniformly to $f$ on the singleton set $\{x\}$ with respect to the filter $p$. 2. The sequence $F_n(x)$ converges to $f(x)$ in $\beta$ with respect to the filter $p$.

Filter.Tendsto.tendstoUniformlyOnFilter_const theorem

 {g : ι → β} {b : β} (hg : Tendsto g p (𝓝 b)) (p' : Filter α) :
  TendstoUniformlyOnFilter (fun n : ι => fun _ : α => g n) (fun _ : α => b) p p'

Full source

/-- 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.tendstoUniformlyOnFilter_const {g : ι → β} {b : β} (hg : Tendsto g p (𝓝 b))
    (p' : Filter α) :
    TendstoUniformlyOnFilter (fun n : ι => fun _ : α => g n) (fun _ : α => b) p p' := by
  simpa only [nhds_eq_comap_uniformity, tendsto_comap_iff] using hg.comp (tendsto_fst (g := p'))

Uniform convergence of constant functions under pointwise convergence

Informal description

Let $\beta$ be a uniform space and $\alpha$ be a topological space. Given a sequence of functions $g_n \colon \iota \to \beta$ converging to $b \in \beta$ with respect to a filter $p$ on $\iota$, the sequence of constant functions $F_n \colon \alpha \to \beta$ defined by $F_n(a) = g_n$ for all $a \in \alpha$ converges uniformly on any filter $p'$ of $\alpha$ to the constant function $f \colon \alpha \to \beta$ defined by $f(a) = b$ for all $a \in \alpha$.

Filter.Tendsto.tendstoUniformlyOn_const theorem

 {g : ι → β} {b : β} (hg : Tendsto g p (𝓝 b)) (s : Set α) :
  TendstoUniformlyOn (fun n : ι => fun _ : α => g n) (fun _ : α => b) p s

Full source

/-- 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 {g : ι → β} {b : β} (hg : Tendsto g p (𝓝 b))
    (s : Set α) : TendstoUniformlyOn (fun n : ι => fun _ : α => g n) (fun _ : α => b) p s :=
  tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr (hg.tendstoUniformlyOnFilter_const (𝓟 s))

Uniform Convergence of Constant Functions on a Set

Informal description

Let $\beta$ be a uniform space, $\alpha$ be a topological space, and $s \subseteq \alpha$ be a subset. If a sequence of functions $g_n \colon \iota \to \beta$ converges to $b \in \beta$ with respect to a filter $p$ on $\iota$, then the sequence of constant functions $F_n \colon \alpha \to \beta$ defined by $F_n(a) = g_n$ for all $a \in \alpha$ converges uniformly on $s$ to the constant function $f \colon \alpha \to \beta$ defined by $f(a) = b$ for all $a \in \alpha$.

UniformContinuousOn.tendstoUniformlyOn theorem

 [UniformSpace α] [UniformSpace γ] {U : Set α} {V : Set β} {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ V))
  (hU : x ∈ U) : TendstoUniformlyOn F (F x) (𝓝[U] x) V

Full source

theorem UniformContinuousOn.tendstoUniformlyOn [UniformSpace α] [UniformSpace γ] {U : Set α}
    {V : Set β} {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ V)) (hU : x ∈ U) :
    TendstoUniformlyOn F (F x) (𝓝[U] x) V := by
  set φ := fun q : α × β => ((x, q.2), q)
  rw [tendstoUniformlyOn_iff_tendsto]
  change Tendsto (Prod.mapProd.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
  simp only [nhdsWithin, Filter.prod_eq_inf, comap_inf, inf_assoc, comap_principal, inf_principal]
  refine hF.comp (Tendsto.inf ?_ <| tendsto_principal_principal.2 fun x hx => ⟨⟨hU, hx.2⟩, hx⟩)
  simp only [uniformity_prod_eq_comap_prod, tendsto_comap_iff, (· ∘ ·),
    nhds_eq_comap_uniformity, comap_comap]
  exact tendsto_comap.prodMk (tendsto_diag_uniformity _ _)

Uniform convergence of uniformly continuous functions on product sets

Informal description

Let $\alpha$ and $\gamma$ be uniform spaces, and let $U \subseteq \alpha$ and $V \subseteq \beta$ be subsets. Suppose $F \colon \alpha \times \beta \to \gamma$ is uniformly continuous on $U \times V$ (where $\timesˢ$ denotes the Cartesian product of sets). Then, for any $x \in U$, the family of functions $F(\cdot, y)$ converges uniformly on $V$ to $F(x, \cdot)$ as the first argument tends to $x$ within $U$. In other words, for any entourage $W$ in the uniformity of $\gamma$, there exists a neighborhood $N$ of $x$ in $U$ such that for all $x' \in N$ and all $y \in V$, the pair $(F(x, y), F(x', y))$ belongs to $W$.

UniformContinuousOn.tendstoUniformly theorem

 [UniformSpace α] [UniformSpace γ] {U : Set α} (hU : U ∈ 𝓝 x) {F : α → β → γ}
  (hF : UniformContinuousOn (↿F) (U ×ˢ (univ : Set β))) : TendstoUniformly F (F x) (𝓝 x)

Full source

theorem UniformContinuousOn.tendstoUniformly [UniformSpace α] [UniformSpace γ] {U : Set α}
    (hU : U ∈ 𝓝 x) {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ (univ : Set β))) :
    TendstoUniformly F (F x) (𝓝 x) := by
  simpa only [tendstoUniformlyOn_univ, nhdsWithin_eq_nhds.2 hU]
    using hF.tendstoUniformlyOn (mem_of_mem_nhds hU)

Uniform Convergence of Uniformly Continuous Functions on Product Spaces

Informal description

Let $\alpha$ and $\gamma$ be uniform spaces, $U \subseteq \alpha$ be a neighborhood of a point $x \in \alpha$, and $F \colon \alpha \times \beta \to \gamma$ be a function. If the uncurried function $\uncurry F$ is uniformly continuous on $U \times \beta$, then the family of functions $F(\cdot, y)$ converges uniformly on $\beta$ to $F(x, \cdot)$ as the first argument tends to $x$. In other words, for any entourage $W$ in the uniformity of $\gamma$, there exists a neighborhood $N$ of $x$ in $U$ such that for all $x' \in N$ and all $y \in \beta$, the pair $(F(x, y), F(x', y))$ belongs to $W$.

UniformContinuous₂.tendstoUniformly theorem

 [UniformSpace α] [UniformSpace γ] {f : α → β → γ} (h : UniformContinuous₂ f) : TendstoUniformly f (f x) (𝓝 x)

Full source

theorem UniformContinuous₂.tendstoUniformly [UniformSpace α] [UniformSpace γ] {f : α → β → γ}
    (h : UniformContinuous₂ f) : TendstoUniformly f (f x) (𝓝 x) :=
  UniformContinuousOn.tendstoUniformly univ_mem <| by rwa [univ_prod_univ, uniformContinuousOn_univ]

Uniform Convergence of Bivariate Uniformly Continuous Functions

Informal description

Let $\alpha$ and $\gamma$ be uniform spaces, and let $f \colon \alpha \times \beta \to \gamma$ be a uniformly continuous function in both arguments. Then, for any $x \in \alpha$, the family of functions $f(\cdot, y)$ converges uniformly on $\beta$ to $f(x, \cdot)$ as the first argument tends to $x$. In other words, for any entourage $W$ in the uniformity of $\gamma$, there exists a neighborhood $N$ of $x$ in $\alpha$ such that for all $x' \in N$ and all $y \in \beta$, the pair $(f(x, y), f(x', y))$ belongs to $W$.

UniformCauchySeqOnFilter definition

(F : ι → α → β) (p : Filter ι) (p' : Filter α) : Prop

Full source

/-- A sequence is uniformly Cauchy if eventually all of its pairwise differences are
uniformly bounded -/
def UniformCauchySeqOnFilter (F : ι → α → β) (p : Filter ι) (p' : Filter α) : Prop :=
  ∀ u ∈ 𝓤 β, ∀ᶠ m : (ι × ι) × α in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u

Uniformly Cauchy family of functions on a filter

Informal description

A family of functions $ F : \iota \to \alpha \to \beta $ is called *uniformly Cauchy on a filter* $ p' $ over $ \alpha $ with respect to a filter $ p $ on $ \iota $ if, for every entourage $ u $ in the uniformity of $ \beta $, there exists an event in $ (p \times p) \times p' $ such that for all pairs $ (m, n) $ in $ p \times p $ and all $ x $ in $ p' $, the pair $ (F_m(x), F_n(x)) $ belongs to $ u $. In other words, for any uniform neighborhood $ u $ of the diagonal in $ \beta \times \beta $, the functions $ F_m $ and $ F_n $ are uniformly $ u $-close on the filter $ p' $ for all sufficiently large $ m $ and $ n $ (as determined by the filter $ p $).

UniformCauchySeqOn definition

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

Full source

/-- A sequence is uniformly Cauchy if eventually all of its pairwise differences are
uniformly bounded -/
def UniformCauchySeqOn (F : ι → α → β) (p : Filter ι) (s : Set α) : Prop :=
  ∀ u ∈ 𝓤 β, ∀ᶠ m : ι × ι in p ×ˢ p, ∀ x : α, x ∈ s → (F m.fst x, F m.snd x) ∈ u

Uniformly Cauchy sequence of functions on a set

Informal description

A sequence of functions $ F_n : \alpha \to \beta $ indexed by $ n \in \iota $ is called *uniformly Cauchy on a set $ s \subseteq \alpha $* with respect to a filter $ p $ on $ \iota $ if, for every entourage $ u $ in the uniformity of $ \beta $, there exists an event in $ p \times p $ such that for all pairs $ (m, n) $ in this event and for all $ x \in s $, the pair $ (F_m(x), F_n(x)) $ belongs to $ u $. In other words, for any uniform neighborhood $ u $ of the diagonal in $ \beta \times \beta $, the functions $ F_m $ and $ F_n $ are uniformly $ u $-close on $ s $ for all sufficiently large $ m $ and $ n $ (as determined by the filter $ p $).

uniformCauchySeqOn_iff_uniformCauchySeqOnFilter theorem

: UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s)

Full source

theorem uniformCauchySeqOn_iff_uniformCauchySeqOnFilter :
    UniformCauchySeqOnUniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s) := by
  simp only [UniformCauchySeqOn, UniformCauchySeqOnFilter]
  refine forall₂_congr fun u hu => ?_
  rw [eventually_prod_principal_iff]

Equivalence of Uniformly Cauchy Conditions on Set and Principal Filter

Informal description

A family of functions $ F : \iota \to \alpha \to \beta $ is uniformly Cauchy on a set $ s \subseteq \alpha $ with respect to a filter $ p $ on $ \iota $ if and only if it is uniformly Cauchy on the principal filter $ \mathfrak{P}(s) $ generated by $ s $. In other words, for every entourage $ u $ in the uniformity of $ \beta $, there exists an event in $ p \times p $ such that for all pairs $ (m, n) $ in this event and all $ x \in s $, the pair $ (F_m(x), F_n(x)) $ belongs to $ u $, if and only if the same condition holds for the principal filter $ \mathfrak{P}(s) $.

UniformCauchySeqOn.uniformCauchySeqOnFilter theorem

(hF : UniformCauchySeqOn F p s) : UniformCauchySeqOnFilter F p (𝓟 s)

Full source

theorem UniformCauchySeqOn.uniformCauchySeqOnFilter (hF : UniformCauchySeqOn F p s) :
    UniformCauchySeqOnFilter F p (𝓟 s) := by rwa [← uniformCauchySeqOn_iff_uniformCauchySeqOnFilter]

Uniformly Cauchy on Set Implies Uniformly Cauchy on Principal Filter

Informal description

If a family of functions $ F : \iota \to \alpha \to \beta $ is uniformly Cauchy on a set $ s \subseteq \alpha $ with respect to a filter $ p $ on $ \iota $, then it is also uniformly Cauchy on the principal filter $ \mathfrak{P}(s) $ generated by $ s $.

TendstoUniformlyOnFilter.uniformCauchySeqOnFilter theorem

(hF : TendstoUniformlyOnFilter F f p p') : UniformCauchySeqOnFilter F p p'

Full source

/-- A sequence that converges uniformly is also uniformly Cauchy -/
theorem TendstoUniformlyOnFilter.uniformCauchySeqOnFilter (hF : TendstoUniformlyOnFilter F f p p') :
    UniformCauchySeqOnFilter F p p' := by
  intro u hu
  rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
  have := tendsto_swap4_prod.eventually ((hF t ht).prod_mk (hF t ht))
  apply this.diag_of_prod_right.mono
  simp only [and_imp, Prod.forall]
  intro n1 n2 x hl hr
  exact Set.mem_of_mem_of_subset (prodMk_mem_compRel (htsymm hl) hr) htmem

Uniform Convergence Implies Uniformly Cauchy Condition on Filter

Informal description

Let $\alpha$ be a topological space, $\beta$ a uniform space, and $F : \iota \to \alpha \to \beta$ a family of functions indexed by $\iota$ with a filter $p$ on $\iota$. If $F$ converges uniformly on a filter $p'$ over $\alpha$ to a function $f : \alpha \to \beta$, then $F$ is uniformly Cauchy on $p'$ with respect to $p$. In other words, for any entourage $u$ in the uniformity of $\beta$, there exists an event in $p \times p$ such that for all pairs $(m, n)$ in this event and all $x$ in $p'$, the pair $(F_m(x), F_n(x))$ belongs to $u$.

TendstoUniformlyOn.uniformCauchySeqOn theorem

(hF : TendstoUniformlyOn F f p s) : UniformCauchySeqOn F p s

Full source

/-- A sequence that converges uniformly is also uniformly Cauchy -/
theorem TendstoUniformlyOn.uniformCauchySeqOn (hF : TendstoUniformlyOn F f p s) :
    UniformCauchySeqOn F p s :=
  uniformCauchySeqOn_iff_uniformCauchySeqOnFilter.mpr
    hF.tendstoUniformlyOnFilter.uniformCauchySeqOnFilter

Uniform convergence implies uniform Cauchy condition on a set

Informal description

Let $\alpha$ be a topological space, $\beta$ a uniform space, and $F : \iota \to \alpha \to \beta$ a family of functions indexed by $\iota$ with a filter $p$ on $\iota$. If $F$ converges uniformly on a set $s \subseteq \alpha$ to a function $f : \alpha \to \beta$, then $F$ is uniformly Cauchy on $s$ with respect to $p$. In other words, for any entourage $u$ in the uniformity of $\beta$, there exists an event in $p \times p$ such that for all pairs $(m, n)$ in this event and all $x \in s$, the pair $(F_m(x), F_n(x))$ belongs to $u$.

UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto theorem

 (hF : UniformCauchySeqOnFilter F p p') (hF' : ∀ᶠ x : α in p', Tendsto (fun n => F n x) p (𝓝 (f x))) :
  TendstoUniformlyOnFilter F f p p'

Full source

/-- A uniformly Cauchy sequence converges uniformly to its limit -/
theorem UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto
    (hF : UniformCauchySeqOnFilter F p p')
    (hF' : ∀ᶠ x : α in p', Tendsto (fun n => F n x) p (𝓝 (f x))) :
    TendstoUniformlyOnFilter F f p p' := by
  rcases p.eq_or_neBot with rfl | _
  · simp only [TendstoUniformlyOnFilter, bot_prod, eventually_bot, implies_true]
  -- Proof idea: |f_n(x) - f(x)| ≤ |f_n(x) - f_m(x)| + |f_m(x) - f(x)|. We choose `n`
  -- so that |f_n(x) - f_m(x)| is uniformly small across `s` whenever `m ≥ n`. Then for
  -- a fixed `x`, we choose `m` sufficiently large such that |f_m(x) - f(x)| is small.
  intro u hu
  rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
  -- We will choose n, x, and m simultaneously. n and x come from hF. m comes from hF'
  -- But we need to promote hF' to the full product filter to use it
  have hmc : ∀ᶠ x in (p ×ˢ p) ×ˢ p', Tendsto (fun n : ι => F n x.snd) p (𝓝 (f x.snd)) := by
    rw [eventually_prod_iff]
    exact ⟨fun _ => True, by simp, _, hF', by simp⟩
  -- To apply filter operations we'll need to do some order manipulation
  rw [Filter.eventually_swap_iff]
  have := tendsto_prodAssoc.eventually (tendsto_prod_swap.eventually ((hF t ht).and hmc))
  apply this.curry.mono
  simp only [Equiv.prodAssoc_apply, eventually_and, eventually_const, Prod.snd_swap, Prod.fst_swap,
    and_imp, Prod.forall]
  -- Complete the proof
  intro x n hx hm'
  refine Set.mem_of_mem_of_subset (mem_compRel.mpr ?_) htmem
  rw [Uniform.tendsto_nhds_right] at hm'
  have := hx.and (hm' ht)
  obtain ⟨m, hm⟩ := this.exists
  exact ⟨F m x, ⟨hm.2, htsymm hm.1⟩⟩

Uniform convergence of a uniformly Cauchy sequence with pointwise limit

Informal description

Let $F : \iota \to \alpha \to \beta$ be a family of functions between a topological space $\alpha$ and a uniform space $\beta$, indexed by $\iota$ with a filter $p$ on $\iota$. Let $p'$ be a filter on $\alpha$ and $f : \alpha \to \beta$ be a function. If: 1. $F$ is uniformly Cauchy on $p'$ with respect to $p$ (i.e., for any entourage $u$ in $\beta$, there exists $A \in p$ such that for all $m, n \in A$ and $x \in p'$, $(F_m(x), F_n(x)) \in u$), and 2. For almost all $x$ in $p'$, the sequence $(F_n(x))_{n \in \iota}$ converges to $f(x)$ with respect to $p$, then $F$ converges uniformly to $f$ on $p'$ with respect to $p$.

UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto theorem

 (hF : UniformCauchySeqOn F p s) (hF' : ∀ x : α, x ∈ s → Tendsto (fun n => F n x) p (𝓝 (f x))) :
  TendstoUniformlyOn F f p s

Full source

/-- A uniformly Cauchy sequence converges uniformly to its limit -/
theorem UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto (hF : UniformCauchySeqOn F p s)
    (hF' : ∀ x : α, x ∈ s → Tendsto (fun n => F n x) p (𝓝 (f x))) : TendstoUniformlyOn F f p s :=
  tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr
    (hF.uniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto hF')

Uniform Convergence of a Uniformly Cauchy Sequence with Pointwise Limit on a Set

Informal description

Let $F : \iota \to \alpha \to \beta$ be a family of functions from a topological space $\alpha$ to a uniform space $\beta$, indexed by $\iota$ with a filter $p$ on $\iota$, and let $s \subseteq \alpha$ be a subset. If: 1. $F$ is uniformly Cauchy on $s$ with respect to $p$ (i.e., for any entourage $u$ in $\beta$, there exists $A \in p$ such that for all $m, n \in A$ and $x \in s$, $(F_m(x), F_n(x)) \in u$), and 2. For every $x \in s$, the sequence $(F_n(x))_{n \in \iota}$ converges to $f(x)$ with respect to $p$, then $F$ converges uniformly to $f$ on $s$ with respect to $p$.

UniformCauchySeqOnFilter.mono_left theorem

{p'' : Filter ι} (hf : UniformCauchySeqOnFilter F p p') (hp : p'' ≤ p) : UniformCauchySeqOnFilter F p'' p'

Full source

theorem UniformCauchySeqOnFilter.mono_left {p'' : Filter ι} (hf : UniformCauchySeqOnFilter F p p')
    (hp : p'' ≤ p) : UniformCauchySeqOnFilter F p'' p' := by
  intro u hu
  have := (hf u hu).filter_mono (p'.prod_mono_left (Filter.prod_mono hp hp))
  exact this.mono (by simp)

Uniform Cauchy condition is preserved under filter refinement in the index set

Informal description

Let $F : \iota \to \alpha \to \beta$ be a family of functions, $p$ and $p'$ be filters on $\iota$ and $\alpha$ respectively. If $F$ is uniformly Cauchy on $p'$ with respect to $p$, and $p''$ is a filter on $\iota$ such that $p'' \leq p$, then $F$ is also uniformly Cauchy on $p'$ with respect to $p''$.

UniformCauchySeqOnFilter.mono_right theorem

{p'' : Filter α} (hf : UniformCauchySeqOnFilter F p p') (hp : p'' ≤ p') : UniformCauchySeqOnFilter F p p''

Full source

theorem UniformCauchySeqOnFilter.mono_right {p'' : Filter α} (hf : UniformCauchySeqOnFilter F p p')
    (hp : p'' ≤ p') : UniformCauchySeqOnFilter F p p'' := fun u hu =>
  have := (hf u hu).filter_mono ((p ×ˢ p).prod_mono_right hp)
  this.mono (by simp)

Uniform Cauchy condition is preserved under filter refinement in the target space

Informal description

Let $F : \iota \to \alpha \to \beta$ be a family of functions, and let $p$ and $p'$ be filters on $\iota$ and $\alpha$ respectively. If $F$ is uniformly Cauchy on $p'$ with respect to $p$, and $p''$ is a filter on $\alpha$ such that $p'' \leq p'$, then $F$ is also uniformly Cauchy on $p''$ with respect to $p$.

UniformCauchySeqOn.mono theorem

(hf : UniformCauchySeqOn F p s) (hss' : s' ⊆ s) : UniformCauchySeqOn F p s'

Full source

theorem UniformCauchySeqOn.mono (hf : UniformCauchySeqOn F p s) (hss' : s' ⊆ s) :
    UniformCauchySeqOn F p s' := by
  rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢
  exact hf.mono_right (le_principal_iff.mpr <| mem_principal.mpr hss')

Uniform Cauchy condition is preserved under restriction to smaller sets

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $F_n \colon \alpha \to \beta$ a family of functions indexed by $\iota$, $p$ a filter on $\iota$, and $s, s' \subseteq \alpha$ with $s' \subseteq s$. If $(F_n)$ is uniformly Cauchy on $s$ with respect to $p$, then $(F_n)$ is also uniformly Cauchy on $s'$ with respect to $p$.

UniformCauchySeqOnFilter.comp theorem

 {γ : Type*} (hf : UniformCauchySeqOnFilter F p p') (g : γ → α) :
  UniformCauchySeqOnFilter (fun n => F n ∘ g) p (p'.comap g)

Full source

/-- Composing on the right by a function preserves uniform Cauchy sequences -/
theorem UniformCauchySeqOnFilter.comp {γ : Type*} (hf : UniformCauchySeqOnFilter F p p')
    (g : γ → α) : UniformCauchySeqOnFilter (fun n => F n ∘ g) p (p'.comap g) := fun u hu => by
  obtain ⟨pa, hpa, pb, hpb, hpapb⟩ := eventually_prod_iff.mp (hf u hu)
  rw [eventually_prod_iff]
  refine ⟨pa, hpa, pb ∘ g, ?_, fun hx _ hy => hpapb hx hy⟩
  exact eventually_comap.mpr (hpb.mono fun x hx y hy => by simp only [hx, hy, Function.comp_apply])

Right Composition Preserves Uniform Cauchy Condition on a Filter

Informal description

Let $\gamma$ be a type, $\alpha$ and $\beta$ uniform spaces, $F_n \colon \alpha \to \beta$ a family of functions, $p$ a filter on the index set, and $p'$ a filter on $\alpha$. If $(F_n)$ is uniformly Cauchy on $p'$ with respect to $p$, and $g \colon \gamma \to \alpha$ is a function, then the family $(F_n \circ g)$ is uniformly Cauchy on the filter $p'$ composed with $g$ (i.e., $p'.\text{comap}(g)$) with respect to $p$.

UniformCauchySeqOn.comp theorem

{γ : Type*} (hf : UniformCauchySeqOn F p s) (g : γ → α) : UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s)

Full source

/-- Composing on the right by a function preserves uniform Cauchy sequences -/
theorem UniformCauchySeqOn.comp {γ : Type*} (hf : UniformCauchySeqOn F p s) (g : γ → α) :
    UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s) := by
  rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢
  simpa only [UniformCauchySeqOn, comap_principal] using hf.comp g

Right Composition Preserves Uniform Cauchy Condition on a Set

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types, with $\alpha$ and $\beta$ endowed with uniform space structures. Let $F_n \colon \alpha \to \beta$ be a sequence of functions, $p$ a filter on the index set $\iota$, and $s \subseteq \alpha$. If $(F_n)$ is uniformly Cauchy on $s$ with respect to $p$, and $g \colon \gamma \to \alpha$ is a function, then the sequence $(F_n \circ g)$ is uniformly Cauchy on the preimage $g^{-1}(s)$ with respect to $p$.

UniformContinuous.comp_uniformCauchySeqOn theorem

 [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (hf : UniformCauchySeqOn F p s) :
  UniformCauchySeqOn (fun n => g ∘ F n) p s

Full source

/-- Composing on the left by a uniformly continuous function preserves
uniform Cauchy sequences -/
theorem UniformContinuous.comp_uniformCauchySeqOn [UniformSpace γ] {g : β → γ}
    (hg : UniformContinuous g) (hf : UniformCauchySeqOn F p s) :
    UniformCauchySeqOn (fun n => g ∘ F n) p s := fun _u hu => hf _ (hg hu)

Uniformly Continuous Function Preserves Uniform Cauchy Sequences

Informal description

Let $\alpha$ be a type, $\beta$ and $\gamma$ uniform spaces, $F_n \colon \alpha \to \beta$ a sequence of functions, $p$ a filter on the index set, and $s \subseteq \alpha$. If $g \colon \beta \to \gamma$ is uniformly continuous and $(F_n)$ is uniformly Cauchy on $s$ with respect to $p$, then the sequence $(g \circ F_n)$ is also uniformly Cauchy on $s$ with respect to $p$.

UniformCauchySeqOn.prodMap theorem

 {ι' α' β' : Type*} [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')

Full source

theorem UniformCauchySeqOn.prodMap {ι' α' β' : Type*} [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') := by
  intro u hu
  rw [uniformity_prod_eq_prod, mem_map, mem_prod_iff] at hu
  obtain ⟨v, hv, w, hw, hvw⟩ := hu
  simp_rw [mem_prod, and_imp, Prod.forall, Prod.map_apply]
  rw [← Set.image_subset_iff] at hvw
  apply (tendsto_swap4_prod.eventually ((h v hv).prod_mk (h' w hw))).mono
  intro x hx a b ha hb
  exact hvw ⟨_, mk_mem_prod (hx.1 a ha) (hx.2 b hb), rfl⟩

Uniform Cauchy Property of Product Sequences on Product Sets

Informal description

Let $\alpha, \alpha', \beta, \beta'$ be types with $\beta$ and $\beta'$ equipped with uniform space structures. Let $F_n : \alpha \to \beta$ and $F'_m : \alpha' \to \beta'$ be sequences of functions indexed by $n \in \iota$ and $m \in \iota'$ respectively. Suppose $F_n$ is uniformly Cauchy on $s \subseteq \alpha$ with respect to filter $p$ on $\iota$, and $F'_m$ is uniformly Cauchy on $s' \subseteq \alpha'$ with respect to filter $p'$ on $\iota'$. Then the product sequence $(F_n \times F'_m) : \alpha \times \alpha' \to \beta \times \beta'$ defined by $(x,y) \mapsto (F_n(x), F'_m(y))$ is uniformly Cauchy on $s \times s'$ with respect to the product filter $p \times p'$ on $\iota \times \iota'$.

UniformCauchySeqOn.prod theorem

 {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'} {p' : Filter ι'} (h : UniformCauchySeqOn F p s)
  (h' : UniformCauchySeqOn F' p' s) : UniformCauchySeqOn (fun (i : ι × ι') a => (F i.fst a, F' i.snd a)) (p ×ˢ p') s

Full source

theorem UniformCauchySeqOn.prod {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'}
    {p' : Filter ι'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s) :
    UniformCauchySeqOn (fun (i : ι × ι') a => (F i.fst a, F' i.snd a)) (p ×ˢ p') s :=
  (congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a))

Uniform Cauchy Property of Product Sequences on a Common Set

Informal description

Let $\alpha$ be a type, and $\beta, \beta'$ be uniform spaces. Let $F_n \colon \alpha \to \beta$ and $F'_m \colon \alpha \to \beta'$ be sequences of functions indexed by $n \in \iota$ and $m \in \iota'$ respectively. Suppose $F_n$ is uniformly Cauchy on a set $s \subseteq \alpha$ with respect to a filter $p$ on $\iota$, and $F'_m$ is uniformly Cauchy on $s$ with respect to a filter $p'$ on $\iota'$. Then the sequence $(F_n \times F'_m) \colon \alpha \to \beta \times \beta'$ defined by $x \mapsto (F_n(x), F'_m(x))$ is uniformly Cauchy on $s$ with respect to the product filter $p \times p'$ on $\iota \times \iota'$.

UniformCauchySeqOn.prod' theorem

 {β' : Type*} [UniformSpace β'] {F' : ι → α → β'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p s) :
  UniformCauchySeqOn (fun (i : ι) a => (F i a, F' i a)) p s

Full source

theorem UniformCauchySeqOn.prod' {β' : Type*} [UniformSpace β'] {F' : ι → α → β'}
    (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p s) :
    UniformCauchySeqOn (fun (i : ι) a => (F i a, F' i a)) p s := fun u hu =>
  have hh : Tendsto (fun x : ι => (x, x)) p (p ×ˢ p) := tendsto_diag
  (hh.prodMap hh).eventually ((h.prod h') u hu)

Uniform Cauchy Property of Pointwise Product Sequences on a Common Set

Informal description

Let $\alpha$ be a type, and $\beta, \beta'$ be uniform spaces. Let $F_n \colon \alpha \to \beta$ and $F'_n \colon \alpha \to \beta'$ be sequences of functions indexed by $n \in \iota$. If both $F_n$ and $F'_n$ are uniformly Cauchy on a set $s \subseteq \alpha$ with respect to the same filter $p$ on $\iota$, then the sequence $(F_n \times F'_n) \colon \alpha \to \beta \times \beta'$ defined by $x \mapsto (F_n(x), F'_n(x))$ is also uniformly Cauchy on $s$ with respect to $p$.

UniformCauchySeqOn.cauchy_map theorem

[hp : NeBot p] (hf : UniformCauchySeqOn F p s) (hx : x ∈ s) : Cauchy (map (fun i => F i x) p)

Full source

/-- If a sequence of functions is uniformly Cauchy on a set, then the values at each point form
a Cauchy sequence. -/
theorem UniformCauchySeqOn.cauchy_map [hp : NeBot p] (hf : UniformCauchySeqOn F p s) (hx : x ∈ s) :
    Cauchy (map (fun i => F i x) p) := by
  simp only [cauchy_map_iff, hp, true_and]
  intro u hu
  rw [mem_map]
  filter_upwards [hf u hu] with p hp using hp x hx

Pointwise Cauchy Property of Uniformly Cauchy Sequences

Informal description

Let $F_n : \alpha \to \beta$ be a sequence of functions indexed by $n \in \iota$, where $\beta$ is a uniform space. If the sequence is uniformly Cauchy on a set $s \subseteq \alpha$ with respect to a non-trivial filter $p$ on $\iota$, then for any point $x \in s$, the sequence of values $(F_n(x))_{n \in \iota}$ is a Cauchy sequence in $\beta$ with respect to the filter $p$.

UniformCauchySeqOn.cauchySeq theorem

[Nonempty ι] [SemilatticeSup ι] (hf : UniformCauchySeqOn F atTop s) (hx : x ∈ s) : CauchySeq fun i ↦ F i x

Full source

/-- 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 UniformCauchySeqOn.cauchySeq [Nonempty ι] [SemilatticeSup ι]
    (hf : UniformCauchySeqOn F atTop s) (hx : x ∈ s) :
    CauchySeq fun i ↦ F i x :=
  hf.cauchy_map (hp := atTop_neBot) hx

Pointwise Cauchy Property of Uniformly Cauchy Sequences with Directed Index Set

Informal description

Let $\alpha$ be a type, $\beta$ a uniform space, and $F_n : \alpha \to \beta$ a sequence of functions indexed by a nonempty directed set $\iota$ with a join-semilattice structure. If the sequence $(F_n)$ is uniformly Cauchy on a set $s \subseteq \alpha$ with respect to the filter `atTop` on $\iota$, then for any point $x \in s$, the sequence of values $(F_n(x))_{n \in \iota}$ is a Cauchy sequence in $\beta$.

tendstoUniformlyOn_of_seq_tendstoUniformlyOn theorem

 {l : Filter ι} [l.IsCountablyGenerated]
  (h : ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s) : TendstoUniformlyOn F f l s

Full source

theorem tendstoUniformlyOn_of_seq_tendstoUniformlyOn {l : Filter ι} [l.IsCountablyGenerated]
    (h : ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s) :
    TendstoUniformlyOn F f l s := by
  rw [tendstoUniformlyOn_iff_tendsto, tendsto_iff_seq_tendsto]
  intro u hu
  rw [tendsto_prod_iff'] at hu
  specialize h (fun n => (u n).fst) hu.1
  rw [tendstoUniformlyOn_iff_tendsto] at h
  exact h.comp (tendsto_id.prodMk hu.2)

Uniform convergence via sequential convergence on countably generated filters

Informal description

Let $\iota$ be an indexing type with a countably generated filter $l$, and let $F_n : \alpha \to \beta$ be a family of functions indexed by $n \in \iota$. Suppose that for every sequence $(u_k)_{k \in \mathbb{N}}$ in $\iota$ converging to $l$, the sequence of functions $(F_{u_k})_{k \in \mathbb{N}}$ converges uniformly on a set $s \subseteq \alpha$ to a function $f : \alpha \to \beta$. Then the entire family $(F_n)_{n \in \iota}$ converges uniformly on $s$ to $f$ with respect to the filter $l$.

TendstoUniformlyOn.seq_tendstoUniformlyOn theorem

 {l : Filter ι} (h : TendstoUniformlyOn F f l s) (u : ℕ → ι) (hu : Tendsto u atTop l) :
  TendstoUniformlyOn (fun n => F (u n)) f atTop s

Full source

theorem TendstoUniformlyOn.seq_tendstoUniformlyOn {l : Filter ι} (h : TendstoUniformlyOn F f l s)
    (u : ℕ → ι) (hu : Tendsto u atTop l) : TendstoUniformlyOn (fun n => F (u n)) f atTop s := by
  rw [tendstoUniformlyOn_iff_tendsto] at h ⊢
  exact h.comp ((hu.comp tendsto_fst).prodMk tendsto_snd)

Uniform convergence of sequences extracted from a uniformly convergent family

Informal description

Let $F_n : \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ that converges uniformly on a set $s \subseteq \alpha$ to a function $f : \alpha \to \beta$ with respect to a filter $l$ on $\iota$. For any sequence $(u_k)_{k \in \mathbb{N}}$ in $\iota$ that converges to $l$, the sequence of functions $(F_{u_k})_{k \in \mathbb{N}}$ converges uniformly on $s$ to $f$ with respect to the filter at infinity on $\mathbb{N}$.

tendstoUniformlyOn_iff_seq_tendstoUniformlyOn theorem

 {l : Filter ι} [l.IsCountablyGenerated] :
  TendstoUniformlyOn F f l s ↔ ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s

Full source

theorem tendstoUniformlyOn_iff_seq_tendstoUniformlyOn {l : Filter ι} [l.IsCountablyGenerated] :
    TendstoUniformlyOnTendstoUniformlyOn F f l s ↔
      ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s :=
  ⟨TendstoUniformlyOn.seq_tendstoUniformlyOn, tendstoUniformlyOn_of_seq_tendstoUniformlyOn⟩

Uniform convergence on a set via sequential convergence for countably generated filters

Informal description

Let $\iota$ be an indexing type with a countably generated filter $l$, let $F_n : \alpha \to \beta$ be a family of functions indexed by $n \in \iota$, and let $f : \alpha \to \beta$ be a function. Then the family $(F_n)$ converges uniformly to $f$ on a set $s \subseteq \alpha$ with respect to the filter $l$ if and only if for every sequence $(u_k)_{k \in \mathbb{N}}$ in $\iota$ that converges to $l$, the sequence of functions $(F_{u_k})$ converges uniformly to $f$ on $s$ with respect to the filter at infinity on $\mathbb{N}$.

tendstoUniformly_iff_seq_tendstoUniformly theorem

 {l : Filter ι} [l.IsCountablyGenerated] :
  TendstoUniformly F f l ↔ ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformly (fun n => F (u n)) f atTop

Full source

theorem tendstoUniformly_iff_seq_tendstoUniformly {l : Filter ι} [l.IsCountablyGenerated] :
    TendstoUniformlyTendstoUniformly F f l ↔
      ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformly (fun n => F (u n)) f atTop := by
  simp_rw [← tendstoUniformlyOn_univ]
  exact tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

Uniform convergence via sequential convergence for countably generated filters

Informal description

Let $\iota$ be an indexing type with a countably generated filter $l$, let $F_n : \alpha \to \beta$ be a family of functions indexed by $n \in \iota$, and let $f : \alpha \to \beta$ be a function. Then the family $(F_n)$ converges uniformly to $f$ with respect to the filter $l$ if and only if for every sequence $(u_k)_{k \in \mathbb{N}}$ in $\iota$ that converges to $l$, the sequence of functions $(F_{u_k})$ converges uniformly to $f$ with respect to the filter at infinity on $\mathbb{N}$.

TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto theorem

 (h1 : TendstoUniformlyOnFilter F f p p') (h2 : ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i))) (h3 : Tendsto L p (𝓝 ℓ)) :
  Tendsto f p' (𝓝 ℓ)

Full source

theorem TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
    (h1 : TendstoUniformlyOnFilter F f p p') (h2 : ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i)))
    (h3 : Tendsto L p (𝓝 ℓ)) : Tendsto f p' (𝓝 ℓ) := by
  rw [tendsto_nhds_left]
  intro s hs
  rw [mem_map, Set.preimage, ← eventually_iff]
  obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs
  have p1 : ∀ᶠ i in p, (L i, ℓ) ∈ t := tendsto_nhds_left.mp h3 ht
  have p2 : ∀ᶠ i in p, ∀ᶠ x in p', (F i x, L i) ∈ t := by
    filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
  have p3 : ∀ᶠ i in p, ∀ᶠ x in p', (f x, F i x) ∈ t := (h1 t ht).curry
  obtain ⟨i, p4, p5, p6⟩ := (p1.and (p2.and p3)).exists
  filter_upwards [p5, p6] with x p5 p6 using hts ⟨F i x, p6, L i, p5, p4⟩

Limit of Uniformly Convergent Family of Functions with Pointwise Limits

Informal description

Let $F_n : \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ converging uniformly on a filter $p'$ to a function $f : \alpha \to \beta$ with respect to a filter $p$ on $\iota$. Suppose that for eventually all $n$ in $p$, the functions $F_n$ tend to $L_n$ along $p'$, and that $L_n$ tends to $\ell$ along $p$. Then $f$ tends to $\ell$ along $p'$.

TendstoUniformly.tendsto_of_eventually_tendsto theorem

 (h1 : TendstoUniformly F f p) (h2 : ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i))) (h3 : Tendsto L p (𝓝 ℓ)) :
  Tendsto f p' (𝓝 ℓ)

Full source

theorem TendstoUniformly.tendsto_of_eventually_tendsto
    (h1 : TendstoUniformly F f p) (h2 : ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i)))
    (h3 : Tendsto L p (𝓝 ℓ)) : Tendsto f p' (𝓝 ℓ) :=
  (h1.tendstoUniformlyOnFilter.mono_right le_top).tendsto_of_eventually_tendsto h2 h3

Limit of Uniformly Convergent Family with Pointwise Limits

Informal description

Let $F_n \colon \alpha \to \beta$ be a family of functions indexed by $n \in \iota$ that converges uniformly to $f \colon \alpha \to \beta$ with respect to a filter $p$ on $\iota$. Suppose that for eventually all $n$ in $p$, the functions $F_n$ tend to $L_n$ along a filter $p'$ on $\alpha$, and that $L_n$ tends to $\ell$ along $p$. Then $f$ tends to $\ell$ along $p'$.

Mathlib.Topology.UniformSpace.UniformConvergence

Main results

Implementation notes

Tags