Topology and uniform structure of uniform convergence #

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

• uniform convergence on α (in the uniform_convergence namespace)
• uniform convergence on a specified family 𝔖 of sets of α (in the uniform_convergence_on namespace), also called 𝔖-convergence

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 Neuman 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 #

• uniform_convergence.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 (β × β)
• uniform_convergence.uniform_space: uniform structure of uniform convergence. This is the uniform_space 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 β.
• uniform_convergence_on.uniform_space: 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 β.

Main statements #

Basic properties #

• uniform_convergence.uniform_continuous_eval: evaluation is uniformly continuous for 𝒰(α, uβ).
• uniform_convergence.t2_space: the topology of uniform convergence on α → β is T₂ if β is T₂.
• uniform_convergence.tendsto_iff_tendsto_uniformly: 𝒰(α, β, uβ) is indeed the uniform structure of uniform convergence
• uniform_convergence_on.uniform_continuous_eval_of_mem: evaluation at a point contained in a set of 𝔖 is uniformly continuous for 𝒱(α, β, 𝔖 uβ)
• uniform_convergence.t2_space: the topology of 𝔖-convergence on α → β is T₂ if β is T₂ and 𝔖 covers α
• uniform_convergence_on.tendsto_iff_tendsto_uniformly_on: 𝒱(α, β, 𝔖 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 uniform_spaces 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 #

• uniform_convergence_on.mono: let u₁, u₂ be two uniform structures on γ and 𝔖₁ 𝔖₂ : set (set α). If u₁ ≤ u₂ and 𝔖₂ ⊆ 𝔖₁ then 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂).
• uniform_convergence_on.infi_eq: if u is a family of uniform structures on γ, then 𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i).
• uniform_convergence_on.comap_eq: if u is a uniform structures on β and f : γ → β, then 𝒱(α, γ, 𝔖, comap f u) = comap (λ 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 uniform_convergence.gc and then rely on the Galois connection API to do most of the work.

Morphism statements (unbundled) #

• uniform_convergence_on.postcomp_uniform_continuous: if f : (γ, uγ) → (β, uβ) is uniformly continuous, then (λ g, f ∘ g) : (α → γ, 𝒱(α, γ, 𝔖, uγ)) → (α → β, 𝒱(α, β, 𝔖, uβ)) is uniformly continuous.
• uniform_convergence_on.postcomp_uniform_inducing: if f : (γ, uγ) → (β, uβ) is a uniform inducing, then (λ g, f ∘ g) : (α → γ, 𝒱(α, γ, 𝔖, uγ)) → (α → β, 𝒱(α, β, 𝔖, uβ)) is a uniform inducing.
• uniform_convergence_on.precomp_uniform_continuous: let f : γ → α, 𝔖 : set (set α), 𝔗 : set (set γ), and assume that ∀ T ∈ 𝔗, f '' T ∈ 𝔖. Then, the function (λ g, g ∘ f) : (α → β, 𝒱(α, β, 𝔖, uβ)) → (γ → β, 𝒱(γ, β, 𝔗 uβ)) is uniformly continuous.

Isomorphism statements (bundled) #

• uniform_convergence_on.congr_right: turn a uniform isomorphism (γ, uγ) ≃ᵤ (β, uβ) into a uniform isomorphism (α → γ, 𝒱(α, γ, 𝔖, uγ)) ≃ᵤ (α → β, 𝒱(α, β, 𝔖, uβ)) by post-composing.
• uniform_convergence_on.congr_left: turn a bijection e : γ ≃ α such that we have both ∀ T ∈ 𝔗, e '' T ∈ 𝔖 and ∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗 into a uniform isomorphism (γ → β, 𝒰(γ, β, uβ)) ≃ᵤ (α → β, 𝒰(α, β, uβ)) by pre-composing.
• uniform_convergence_on.uniform_equiv_Pi_comm: the natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform isomorphism between (α → (Π i, δ i), 𝒱(α, (Π i, δ i), 𝔖, (Π i, uδ i))) and ((Π i, α → δ i), (Π i, 𝒱(α, δ i, 𝔖, uδ i))).

Important use cases #

• If (G, uG) is a uniform group, then (α → G, 𝒱(α, G, 𝔖, uG)) is a uniform group: since (/) : G × G → G is uniformly continuous, uniform_convergence_on.postcomp_uniform_continuous tells us that ((/) ∘ —) : (α → G × G) → (α → G) is uniformly continuous. By precomposing with uniform_convergence_on.uniform_equiv_prod_arrow, 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 uniform_convergence_on.precomp_uniform_continuous.

Implementation details #

We do not declare these structures as instances, since they would conflict with Pi.uniform_space.

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 𝔖.
• Add a type synonym for α → β endowed with the structures of uniform convergence?

References #

• N. Bourbaki, General Topology, Chapter X

Tags #

uniform convergence