Locally uniform convergence #
We define a sequence of functions Fₙ to converge locally uniformly to a limiting function f
with respect to a filter p, spelled TendstoLocallyUniformly F f p, if for any x ∈ s and any
entourage of the diagonal u, there is a neighbourhood v of x such that p-eventually we have
(f y, Fₙ y) ∈ u for all y ∈ v.
It is important to note that this definition is somewhat non-standard; it is not in general
equivalent to "every point has a neighborhood on which the convergence is uniform", which is the
definition more commonly encountered in the literature. The reason is that in our definition the
neighborhood v of x can depend on the entourage u; so our condition is a priori weaker than
the usual one, although the two conditions are equivalent if the domain is locally compact.
We adopt this weaker condition because it is more general but apppears to be sufficient for the standard applications of locally-uniform convergence (in particular, for proving that a locally-uniform limit of continuous functions is continuous).
We also define variants for locally uniform convergence on a subset, called
TendstoLocallyUniformlyOn F f p s.
Tags #
Uniform limit, uniform convergence, tends uniformly to
def
TendstoLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
(F : ι → α → β)
(f : α → β)
(p : Filter ι)
(s : Set α)
:
A sequence of functions Fₙ converges locally uniformly on a set s to a limiting function
f with respect to a filter p if, for any entourage of the diagonal u, for any x ∈ s, one
has p-eventually (f y, Fₙ y) ∈ u for all y in a neighborhood of x in s.
Equations
- TendstoLocallyUniformlyOn F f p s = ∀ u ∈ uniformity β, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Instances For
def
TendstoLocallyUniformly
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
(F : ι → α → β)
(f : α → β)
(p : Filter ι)
:
A sequence of functions Fₙ converges locally uniformly to a limiting function f with respect
to a filter p if, for any entourage of the diagonal u, for any x, one has p-eventually
(f y, Fₙ y) ∈ u for all y in a neighborhood of x.
Equations
Instances For
theorem
tendstoLocallyUniformlyOn_univ
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
:
theorem
tendstoLocallyUniformlyOn_iff_forall_tendsto
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
:
TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhdsWithin x s) (uniformity β)
theorem
IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
(hs : IsOpen s)
:
TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhds x) (uniformity β)
theorem
tendstoLocallyUniformly_iff_forall_tendsto
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
:
TendstoLocallyUniformly F f p ↔ ∀ (x : α), Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhds x) (uniformity β)
theorem
tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
:
TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun (i : ι) (x : ↑s) => F i ↑x) (f ∘ Subtype.val) p
theorem
TendstoUniformlyOn.tendstoLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
(h : TendstoUniformlyOn F f p s)
:
TendstoLocallyUniformlyOn F f p s
theorem
TendstoUniformly.tendstoLocallyUniformly
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
(h : TendstoUniformly F f p)
:
TendstoLocallyUniformly F f p
theorem
TendstoLocallyUniformlyOn.mono
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s s' : Set α}
{p : Filter ι}
(h : TendstoLocallyUniformlyOn F f p s)
(h' : s' ⊆ s)
:
TendstoLocallyUniformlyOn F f p s'
theorem
tendstoLocallyUniformlyOn_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
{ι' : Sort u_5}
{S : ι' → Set α}
(hS : ∀ (i : ι'), IsOpen (S i))
(h : ∀ (i : ι'), TendstoLocallyUniformlyOn F f p (S i))
:
TendstoLocallyUniformlyOn F f p (⋃ (i : ι'), S i)
theorem
tendstoLocallyUniformlyOn_biUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
{s : Set γ}
{S : γ → Set α}
(hS : ∀ i ∈ s, IsOpen (S i))
(h : ∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i))
:
TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i)
theorem
tendstoLocallyUniformlyOn_sUnion
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
(S : Set (Set α))
(hS : ∀ s ∈ S, IsOpen s)
(h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s)
:
TendstoLocallyUniformlyOn F f p (⋃₀ S)
theorem
TendstoLocallyUniformlyOn.union
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s s' : Set α}
{p : Filter ι}
(hs₁ : IsOpen s)
(hs₂ : IsOpen s')
(h₁ : TendstoLocallyUniformlyOn F f p s)
(h₂ : TendstoLocallyUniformlyOn F f p s')
:
TendstoLocallyUniformlyOn F f p (s ∪ s')
theorem
TendstoLocallyUniformly.tendstoLocallyUniformlyOn
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
(h : TendstoLocallyUniformly F f p)
:
TendstoLocallyUniformlyOn F f p s
theorem
tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
[CompactSpace α]
:
On a compact space, locally uniform convergence is just uniform convergence.
theorem
tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
(hs : IsCompact s)
:
For a compact set s, locally uniform convergence on s is just uniform convergence on s.
theorem
TendstoLocallyUniformlyOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
[TopologicalSpace γ]
{t : Set γ}
(h : TendstoLocallyUniformlyOn F f p s)
(g : γ → α)
(hg : Set.MapsTo g t s)
(cg : ContinuousOn g t)
:
TendstoLocallyUniformlyOn (fun (n : ι) => F n ∘ g) (f ∘ g) p t
theorem
TendstoLocallyUniformly.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
[TopologicalSpace γ]
(h : TendstoLocallyUniformly F f p)
(g : γ → α)
(cg : Continuous g)
:
TendstoLocallyUniformly (fun (n : ι) => F n ∘ g) (f ∘ g) p
theorem
tendstoLocallyUniformlyOn_TFAE
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{s : Set α}
[LocallyCompactSpace α]
(G : ι → α → β)
(g : α → β)
(p : Filter ι)
(hs : IsOpen s)
:
[TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K, ∀ x ∈ s, ∃ v ∈ nhdsWithin x s, TendstoUniformlyOn G g p v].TFAE
theorem
tendstoLocallyUniformlyOn_iff_forall_isCompact
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
[LocallyCompactSpace α]
(hs : IsOpen s)
:
theorem
tendstoLocallyUniformly_iff_forall_isCompact
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
[LocallyCompactSpace α]
:
theorem
tendstoLocallyUniformlyOn_iff_filter
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
:
theorem
tendstoLocallyUniformly_iff_filter
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{p : Filter ι}
:
theorem
TendstoLocallyUniformlyOn.tendsto_at
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
(hf : TendstoLocallyUniformlyOn F f p s)
{a : α}
(ha : a ∈ s)
:
Filter.Tendsto (fun (i : ι) => F i a) p (nhds (f a))
theorem
TendstoLocallyUniformlyOn.unique
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
[p.NeBot]
[T2Space β]
{g : α → β}
(hf : TendstoLocallyUniformlyOn F f p s)
(hg : TendstoLocallyUniformlyOn F g p s)
:
Set.EqOn f g s
theorem
TendstoLocallyUniformlyOn.congr
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
{G : ι → α → β}
(hf : TendstoLocallyUniformlyOn F f p s)
(hg : ∀ (n : ι), Set.EqOn (F n) (G n) s)
:
TendstoLocallyUniformlyOn G f p s
theorem
TendstoLocallyUniformlyOn.congr_right
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[TopologicalSpace α]
[UniformSpace β]
{F : ι → α → β}
{f : α → β}
{s : Set α}
{p : Filter ι}
{g : α → β}
(hf : TendstoLocallyUniformlyOn F f p s)
(hg : Set.EqOn f g s)
:
TendstoLocallyUniformlyOn F g p s