mathlib3 documentation

topology.algebra.uniform_convergence

Algebraic facts about the topology of uniform convergence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains algebraic compatibility results about the uniform structure of uniform convergence / 𝔖-convergence. They will mostly be useful for defining strong topologies on the space of continuous linear maps between two topological vector spaces.

Main statements #

Implementation notes #

Like in topology/uniform_space/uniform_convergence_topology, we use the type aliases uniform_fun (denoted α →ᵤ β) and uniform_on_fun (denoted α →ᵤ[𝔖] β) for functions from α to β endowed with the structures of uniform convergence and 𝔖-convergence.

TODO #

References #

Tags #

uniform convergence, strong dual

@[protected, instance]
def uniform_fun.add_monoid {α : Type u_1} {β : Type u_2} [add_monoid β] :
Equations
@[protected, instance]
def uniform_fun.monoid {α : Type u_1} {β : Type u_2} [monoid β] :
Equations
@[protected, instance]
def uniform_on_fun.monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [monoid β] :
monoid (uniform_on_fun α β 𝔖)
Equations
@[protected, instance]
def uniform_on_fun.add_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_monoid β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def uniform_fun.comm_monoid {α : Type u_1} {β : Type u_2} [comm_monoid β] :
Equations
@[protected, instance]
def uniform_on_fun.add_comm_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_comm_monoid β] :
Equations
@[protected, instance]
def uniform_on_fun.comm_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [comm_monoid β] :
Equations
@[protected, instance]
def uniform_fun.group {α : Type u_1} {β : Type u_2} [group β] :
Equations
@[protected, instance]
def uniform_fun.add_group {α : Type u_1} {β : Type u_2} [add_group β] :
Equations
@[protected, instance]
def uniform_on_fun.add_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_group β] :
Equations
@[protected, instance]
def uniform_on_fun.group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [group β] :
group (uniform_on_fun α β 𝔖)
Equations
@[protected, instance]
def uniform_fun.comm_group {α : Type u_1} {β : Type u_2} [comm_group β] :
Equations
@[protected, instance]
def uniform_fun.add_comm_group {α : Type u_1} {β : Type u_2} [add_comm_group β] :
Equations
@[protected, instance]
def uniform_on_fun.add_comm_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_comm_group β] :
Equations
@[protected, instance]
def uniform_on_fun.comm_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [comm_group β] :
Equations
@[protected, instance]
def uniform_fun.module {α : Type u_1} {β : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid β] [module R β] :
Equations
@[protected, instance]
def uniform_on_fun.module {α : Type u_1} {β : Type u_2} {R : Type u_4} {𝔖 : set (set α)} [semiring R] [add_comm_monoid β] [module R β] :
module R (uniform_on_fun α β 𝔖)
Equations
@[protected, instance]

If G is a uniform group, then α →ᵤ G is a uniform group as well.

@[protected, instance]

If G is a uniform additive group, then α →ᵤ G is a uniform additive group as well.

@[protected]
theorem uniform_fun.has_basis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [group G] [uniform_space G] [uniform_group G] {p : ι Prop} {b : ι set G} (h : (nhds 1).has_basis p b) :
(nhds 1).has_basis p (λ (i : ι), {f : uniform_fun α G | (x : α), f x b i})
@[protected]
theorem uniform_fun.has_basis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [add_group G] [uniform_space G] [uniform_add_group G] {p : ι Prop} {b : ι set G} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis p (λ (i : ι), {f : uniform_fun α G | (x : α), f x b i})
@[protected]
theorem uniform_fun.has_basis_nhds_zero {α : Type u_1} {G : Type u_2} [add_group G] [uniform_space G] [uniform_add_group G] :
(nhds 0).has_basis (λ (V : set G), V nhds 0) (λ (V : set G), {f : α G | (x : α), f x V})
@[protected]
theorem uniform_fun.has_basis_nhds_one {α : Type u_1} {G : Type u_2} [group G] [uniform_space G] [uniform_group G] :
(nhds 1).has_basis (λ (V : set G), V nhds 1) (λ (V : set G), {f : α G | (x : α), f x V})
@[protected, instance]

Let 𝔖 : set (set α). If G is a uniform additive group, then α →ᵤ[𝔖] G is a uniform additive group as well.

@[protected, instance]
def uniform_on_fun.uniform_group {α : Type u_1} {G : Type u_2} [group G] {𝔖 : set (set α)} [uniform_space G] [uniform_group G] :

Let 𝔖 : set (set α). If G is a uniform group, then α →ᵤ[𝔖] G is a uniform group as well.

@[protected]
theorem uniform_on_fun.has_basis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [group G] [uniform_space G] [uniform_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) {p : ι Prop} {b : ι set G} (h : (nhds 1).has_basis p b) :
(nhds 1).has_basis (λ (Si : set α × ι), Si.fst 𝔖 p Si.snd) (λ (Si : set α × ι), {f : uniform_on_fun α G 𝔖 | (x : α), x Si.fst f x b Si.snd})
@[protected]
theorem uniform_on_fun.has_basis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [add_group G] [uniform_space G] [uniform_add_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) {p : ι Prop} {b : ι set G} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis (λ (Si : set α × ι), Si.fst 𝔖 p Si.snd) (λ (Si : set α × ι), {f : uniform_on_fun α G 𝔖 | (x : α), x Si.fst f x b Si.snd})
@[protected]
theorem uniform_on_fun.has_basis_nhds_one {α : Type u_1} {G : Type u_2} [group G] [uniform_space G] [uniform_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) :
(nhds 1).has_basis (λ (SV : set α × set G), SV.fst 𝔖 SV.snd nhds 1) (λ (SV : set α × set G), {f : uniform_on_fun α G 𝔖 | (x : α), x SV.fst f x SV.snd})
@[protected]
theorem uniform_on_fun.has_basis_nhds_zero {α : Type u_1} {G : Type u_2} [add_group G] [uniform_space G] [uniform_add_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) :
(nhds 0).has_basis (λ (SV : set α × set G), SV.fst 𝔖 SV.snd nhds 0) (λ (SV : set α × set G), {f : uniform_on_fun α G 𝔖 | (x : α), x SV.fst f x SV.snd})
theorem uniform_on_fun.has_continuous_smul_induced_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [normed_field 𝕜] [add_comm_group H] [module 𝕜 H] [add_comm_group E] [module 𝕜 E] [topological_space H] [uniform_space E] [uniform_add_group E] [has_continuous_smul 𝕜 E] {𝔖 : set (set α)} [linear_map_class hom 𝕜 H (uniform_on_fun α E 𝔖)] (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) (φ : hom) (hφ : inducing φ) (h : (u : H) (s : set α), s 𝔖 bornology.is_vonN_bounded 𝕜 (φ u '' s)) :

Let E be a TVS, 𝔖 : set (set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of bornology.is_vonN_bounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

For convenience, we don't literally ask for H : submodule (α →ᵤ[𝔖] E). Instead, we prove the result for any vector space H equipped with a linear inducing to α →ᵤ[𝔖] E, which is often easier to use. We also state the submodule version as uniform_on_fun.has_continuous_smul_submodule_of_image_bounded.

theorem uniform_on_fun.has_continuous_smul_submodule_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [uniform_space E] [uniform_add_group E] [has_continuous_smul 𝕜 E] {𝔖 : set (set α)} (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) (H : submodule 𝕜 (uniform_on_fun α E 𝔖)) (h : (u : α E), u H (s : set α), s 𝔖 bornology.is_vonN_bounded 𝕜 (u '' s)) :

Let E be a TVS, 𝔖 : set (set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of bornology.is_vonN_bounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

If you have a hard time using this lemma, try the one above instead.