Topology and uniform structure of uniform convergence #

This files endows α → β with the topologies / uniform structures of

uniform convergence on α
uniform convergence on a specified family 𝔖 of sets of α, also called 𝔖-convergence

Since α → β is already endowed with the topologies and uniform structures of pointwise convergence, we introduce type aliases UniformFun α β (denoted α →ᵤ β) and UniformOnFun α β 𝔖 (denoted α →ᵤ[𝔖] β) and we actually endow these with the structures of uniform and 𝔖-convergence respectively.

Usual examples of the second construction include :

the topology of compact convergence, when 𝔖 is the set of compacts of α
the strong topology on the dual of a topological vector space (TVS) E, when 𝔖 is the set of Von Neumann bounded subsets of E
the weak-* topology on the dual of a TVS E, when 𝔖 is the set of singletons of E.

This file contains a lot of technical facts, so it is heavily commented, proofs included!

Main definitions #

UniformFun.gen: basis sets for the uniformity of uniform convergence. These are sets of the form S(V) := {(f, g) | ∀ x : α, (f x, g x) ∈ V} for some V : Set (β × β)
UniformFun.uniformSpace: uniform structure of uniform convergence. This is the UniformSpace on α →ᵤ β whose uniformity is generated by the sets S(V) for V ∈ 𝓤 β. We will denote this uniform space as 𝒰(α, β, uβ), both in the comments and as a local notation in the Lean code, where uβ is the uniform space structure on β. This is declared as an instance on α →ᵤ β.
UniformOnFun.uniformSpace: uniform structure of 𝔖-convergence, where 𝔖 : Set (Set α). This is the infimum, for S ∈ 𝔖, of the pullback of 𝒰 S β by the map of restriction to S. We will denote it 𝒱(α, β, 𝔖, uβ), where uβ is the uniform space structure on β. This is declared as an instance on α →ᵤ[𝔖] β.

Main statements #

Basic properties #

UniformFun.uniformContinuous_eval: evaluation is uniformly continuous on α →ᵤ β.
UniformFun.t2Space: the topology of uniform convergence on α →ᵤ β is T₂ if β is T₂.
UniformFun.tendsto_iff_tendstoUniformly: 𝒰(α, β, uβ) is indeed the uniform structure of uniform convergence
UniformOnFun.uniformContinuous_eval_of_mem: evaluation at a point contained in a set of 𝔖 is uniformly continuous on α →ᵤ[𝔖] β
UniformOnFun.t2Space_of_covering: the topology of 𝔖-convergence on α →ᵤ[𝔖] β is T₂ if β is T₂ and 𝔖 covers α
UniformOnFun.tendsto_iff_tendstoUniformlyOn: 𝒱(α, β, 𝔖 uβ) is indeed the uniform structure of 𝔖-convergence

Functoriality and compatibility with product of uniform spaces #

In order to avoid the need for filter bases as much as possible when using these definitions, we develop an extensive API for manipulating these structures abstractly. As usual in the topology section of mathlib, we first state results about the complete lattices of UniformSpaces on fixed types, and then we use these to deduce categorical-like results about maps between two uniform spaces.

We only describe these in the harder case of 𝔖-convergence, as the names of the corresponding results for uniform convergence can easily be guessed.

Order statements #

UniformOnFun.mono: let u₁, u₂ be two uniform structures on γ and 𝔖₁ 𝔖₂ : Set (Set α). If u₁ ≤ u₂ and 𝔖₂ ⊆ 𝔖₁ then 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂).
UniformOnFun.iInf_eq: if u is a family of uniform structures on γ, then 𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i).
UniformOnFun.comap_eq: if u is a uniform structures on β and f : γ → β, then 𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁).

An interesting note about these statements is that they are proved without ever unfolding the basis definition of the uniform structure of uniform convergence! Instead, we build a (not very interesting) Galois connection UniformFun.gc and then rely on the Galois connection API to do most of the work.

Morphism statements (unbundled) #

UniformOnFun.postcomp_uniformContinuous: if f : γ → β is uniformly continuous, then (fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is uniformly continuous.
UniformOnFun.postcomp_uniformInducing: if f : γ → β is a uniform inducing, then (fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is a uniform inducing.
UniformOnFun.precomp_uniformContinuous: let f : γ → α, 𝔖 : Set (Set α), 𝔗 : Set (Set γ), and assume that ∀ T ∈ 𝔗, f '' T ∈ 𝔖. Then, the function (fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β) is uniformly continuous.

Isomorphism statements (bundled) #

UniformOnFun.congrRight: turn a uniform isomorphism γ ≃ᵤ β into a uniform isomorphism (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β) by post-composing.
UniformOnFun.congrLeft: turn a bijection e : γ ≃ α such that we have both ∀ T ∈ 𝔗, e '' T ∈ 𝔖 and ∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗 into a uniform isomorphism (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β) by pre-composing.
UniformOnFun.uniformEquivPiComm: the natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform isomorphism between α →ᵤ[𝔖] (Π i, δ i) and Π i, α →ᵤ[𝔖] δ i.

Important use cases #

If G is a uniform group, then α →ᵤ[𝔖] G is a uniform group: since (/) : G × G → G is uniformly continuous, UniformOnFun.postcomp_uniformContinuous tells us that ((/) ∘ —) : (α →ᵤ[𝔖] G × G) → (α →ᵤ[𝔖] G) is uniformly continuous. By precomposing with UniformOnFun.uniformEquivProdArrow, this gives that (/) : (α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G) → (α →ᵤ[𝔖] G) is also uniformly continuous
The transpose of a continuous linear map is continuous for the strong topologies: since continuous linear maps are uniformly continuous and map bounded sets to bounded sets, this is just a special case of UniformOnFun.precomp_uniformContinuous.

TODO #

Show that the uniform structure of 𝔖-convergence is exactly the structure of 𝔖'-convergence, where 𝔖' is the noncovering bornology (i.e not what Bornology currently refers to in mathlib) generated by 𝔖.

References #

[N. Bourbaki, General Topology, Chapter X][bourbaki1966]

Tags #

uniform convergence