feat(UniformSpace/CompactConvergence): prove metrizability (#10942)

Author: urkud

Mathlib.lean

@@ -3927,6 +3927,7 @@ import Mathlib.Topology.MetricSpace.ShrinkingLemma
 import Mathlib.Topology.MetricSpace.ThickenedIndicator
 import Mathlib.Topology.MetricSpace.Thickening
 import Mathlib.Topology.Metrizable.Basic
+import Mathlib.Topology.Metrizable.ContinuousMap
 import Mathlib.Topology.Metrizable.Uniformity
 import Mathlib.Topology.Metrizable.Urysohn
 import Mathlib.Topology.NhdsSet

Mathlib/MeasureTheory/Constructions/Polish.lean

@@ -946,11 +946,8 @@ theorem measurableSet_exists_tendsto [TopologicalSpace γ] [PolishSpace γ] [Mea
   rcases l.exists_antitone_basis with ⟨u, hu⟩
   simp_rw [← cauchy_map_iff_exists_tendsto]
   change MeasurableSet { x | _ ∧ _ }
-  have :
-    ∀ x,
-      (map (fun i => f i x) l ×ˢ map (fun i => f i x) l).HasAntitoneBasis fun n =>
-        ((fun i => f i x) '' u n) ×ˢ ((fun i => f i x) '' u n) :=
-    fun x => hu.map.prod hu.map
+  have : ∀ x, (map (f · x) l ×ˢ map (f · x) l).HasAntitoneBasis fun n =>
+      ((f · x) '' u n) ×ˢ ((f · x) '' u n) := fun x => (hu.map _).prod (hu.map _)
   simp_rw [and_iff_right (hl.map _),
     Filter.HasBasis.le_basis_iff (this _).toHasBasis Metric.uniformity_basis_dist_inv_nat_succ,
     Set.setOf_forall]

Mathlib/Order/Filter/Bases.lean

@@ -850,11 +850,15 @@ structure HasAntitoneBasis (l : Filter α) (s : ι'' → Set α)
   protected antitone : Antitone s
 #align filter.has_antitone_basis Filter.HasAntitoneBasis
 
-theorem HasAntitoneBasis.map {l : Filter α} {s : ι'' → Set α} {m : α → β}
-    (hf : HasAntitoneBasis l s) : HasAntitoneBasis (map m l) fun n => m '' s n :=
+protected theorem HasAntitoneBasis.map {l : Filter α} {s : ι'' → Set α}
+    (hf : HasAntitoneBasis l s) (m : α → β) : HasAntitoneBasis (map m l) (m '' s ·) :=
   ⟨HasBasis.map _ hf.toHasBasis, fun _ _ h => image_subset _ <| hf.2 h⟩
 #align filter.has_antitone_basis.map Filter.HasAntitoneBasis.map
 
+protected theorem HasAntitoneBasis.comap {l : Filter α} {s : ι'' → Set α}
+    (hf : HasAntitoneBasis l s) (m : β → α) : HasAntitoneBasis (comap m l) (m ⁻¹' s ·) :=
+  ⟨hf.1.comap _, fun _ _ h ↦ preimage_mono (hf.2 h)⟩
+
 lemma HasAntitoneBasis.iInf_principal {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
     {s : ι → Set α} (hs : Antitone s) : (⨅ i, 𝓟 (s i)).HasAntitoneBasis s :=
   ⟨hasBasis_iInf_principal hs.directed_ge, hs⟩
@@ -1026,6 +1030,10 @@ theorem HasCountableBasis.isCountablyGenerated {f : Filter α} {p : ι → Prop}
   ⟨⟨{ t | ∃ i, p i ∧ s i = t }, h.countable.image s, h.toHasBasis.eq_generate⟩⟩
 #align filter.has_countable_basis.is_countably_generated Filter.HasCountableBasis.isCountablyGenerated
 
+theorem HasBasis.isCountablyGenerated [Countable ι] {f : Filter α} {p : ι → Prop} {s : ι → Set α}
+    (h : f.HasBasis p s) : f.IsCountablyGenerated :=
+  HasCountableBasis.isCountablyGenerated ⟨h, to_countable _⟩
+
 theorem antitone_seq_of_seq (s : ℕ → Set α) :
     ∃ t : ℕ → Set α, Antitone t ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (t i) := by
   use fun n => ⋂ m ≤ n, s m; constructor
@@ -1128,21 +1136,20 @@ instance Inf.isCountablyGenerated (f g : Filter α) [IsCountablyGenerated f]
 instance map.isCountablyGenerated (l : Filter α) [l.IsCountablyGenerated] (f : α → β) :
     (map f l).IsCountablyGenerated :=
   let ⟨_x, hxl⟩ := l.exists_antitone_basis
-  HasCountableBasis.isCountablyGenerated ⟨hxl.map.1, to_countable _⟩
+  (hxl.map _).isCountablyGenerated
 #align filter.map.is_countably_generated Filter.map.isCountablyGenerated
 
 instance comap.isCountablyGenerated (l : Filter β) [l.IsCountablyGenerated] (f : α → β) :
     (comap f l).IsCountablyGenerated :=
   let ⟨_x, hxl⟩ := l.exists_antitone_basis
-  HasCountableBasis.isCountablyGenerated ⟨hxl.1.comap _, to_countable _⟩
+  (hxl.comap _).isCountablyGenerated
 #align filter.comap.is_countably_generated Filter.comap.isCountablyGenerated
 
 instance Sup.isCountablyGenerated (f g : Filter α) [IsCountablyGenerated f]
     [IsCountablyGenerated g] : IsCountablyGenerated (f ⊔ g) := by
   rcases f.exists_antitone_basis with ⟨s, hs⟩
   rcases g.exists_antitone_basis with ⟨t, ht⟩
-  exact
-    HasCountableBasis.isCountablyGenerated ⟨hs.1.sup ht.1, Set.to_countable _⟩
+  exact HasCountableBasis.isCountablyGenerated ⟨hs.1.sup ht.1, Set.to_countable _⟩
 #align filter.sup.is_countably_generated Filter.Sup.isCountablyGenerated
 
 instance prod.isCountablyGenerated (la : Filter α) (lb : Filter β) [IsCountablyGenerated la]
@@ -1157,7 +1164,7 @@ instance coprod.isCountablyGenerated (la : Filter α) (lb : Filter β) [IsCounta
 
 end IsCountablyGenerated
 
-theorem isCountablyGenerated_seq [Countable β] (x : β → Set α) :
+theorem isCountablyGenerated_seq [Countable ι'] (x : ι' → Set α) :
     IsCountablyGenerated (⨅ i, 𝓟 (x i)) := by
   use range x, countable_range x
   rw [generate_eq_biInf, iInf_range]

Mathlib/Topology/Algebra/UniformGroup.lean

@@ -922,7 +922,7 @@ instance QuotientGroup.completeSpace' (G : Type u) [Group G] [TopologicalSpace G
   letI : UniformSpace G := TopologicalGroup.toUniformSpace G
   haveI : (𝓤 (G ⧸ N)).IsCountablyGenerated := comap.isCountablyGenerated _ _
   obtain ⟨u, hu, u_mul⟩ := TopologicalGroup.exists_antitone_basis_nhds_one G
-  obtain ⟨hv, v_anti⟩ := @HasAntitoneBasis.map _ _ _ _ _ _ ((↑) : G → G ⧸ N) hu
+  obtain ⟨hv, v_anti⟩ := hu.map ((↑) : G → G ⧸ N)
   rw [← QuotientGroup.nhds_eq N 1, QuotientGroup.mk_one] at hv
   refine' UniformSpace.complete_of_cauchySeq_tendsto fun x hx => _
   /- Given `n : ℕ`, for sufficiently large `a b : ℕ`, given any lift of `x b`, we can find a lift

Mathlib/Topology/Compactness/SigmaCompact.lean

@@ -378,6 +378,15 @@ theorem exists_mem (x : X) : ∃ n, x ∈ K n :=
   iUnion_eq_univ_iff.1 K.iUnion_eq x
 #align compact_exhaustion.exists_mem CompactExhaustion.exists_mem
 
+/-- A compact exhaustion eventually covers any compact set. -/
+theorem exists_superset_of_isCompact {s : Set X} (hs : IsCompact s) : ∃ n, s ⊆ K n := by
+  suffices ∃ n, s ⊆ interior (K n) from this.imp fun _ ↦ (Subset.trans · interior_subset)
+  refine hs.elim_directed_cover (interior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_
+  · intro x _
+    rcases K.exists_mem x with ⟨k, hk⟩
+    exact mem_iUnion.2 ⟨k + 1, K.subset_interior_succ _ hk⟩
+  · exact Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h
+
 /-- The minimal `n` such that `x ∈ K n`. -/
 protected noncomputable def find (x : X) : ℕ :=
   Nat.find (K.exists_mem x)

Mathlib/Topology/Metrizable/ContinuousMap.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.Metrizable.Uniformity
+import Mathlib.Topology.UniformSpace.CompactConvergence
+
+/-!
+# Metrizability of `C(X, Y)`
+
+If `X` is a weakly locally compact σ-compact space and `Y` is a (pseudo)metrizable space,
+then `C(X, Y)` is a (pseudo)metrizable space.
+-/
+
+open TopologicalSpace
+
+namespace ContinuousMap
+
+variable {X Y : Type*}
+  [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X]
+  [TopologicalSpace Y]
+
+instance [PseudoMetrizableSpace Y] : PseudoMetrizableSpace C(X, Y) :=
+  let _ := pseudoMetrizableSpacePseudoMetric Y
+  inferInstance
+
+instance [MetrizableSpace Y] : MetrizableSpace C(X, Y) :=
+  let _ := metrizableSpaceMetric Y
+  UniformSpace.metrizableSpace
+
+end ContinuousMap

Mathlib/Topology/UniformSpace/CompactConvergence.lean

@@ -79,8 +79,6 @@ so that the resulting instance uses the compact-open topology.
 
 ## TODO
 
-* When `α` is compact and `β` is a metric space,
-  the compact-convergence topology (and thus also the compact-open topology) is metrisable.
 * Results about uniformly continuous functions `γ → C(α, β)`
   and uniform limits of sequences `ι → γ → C(α, β)`.
 -/
@@ -223,6 +221,34 @@ theorem mem_compactConvergence_entourage_iff (X : Set (C(α, β) × C(α, β)))
   simp [hasBasis_compactConvergenceUniformity.mem_iff, and_assoc]
 #align continuous_map.mem_compact_convergence_entourage_iff ContinuousMap.mem_compactConvergence_entourage_iff
 
+/-- If `K` is a compact exhaustion of `α`
+and `V i` bounded by `p i` is a basis of entourages of `β`,
+then `fun (n, i) ↦ {(f, g) | ∀ x ∈ K n, (f x, g x) ∈ V i}` bounded by `p i`
+is a basis of entourages of `C(α, β)`. -/
+theorem _root_.CompactExhaustion.hasBasis_compactConvergenceUniformity {ι : Type*}
+    {p : ι → Prop} {V : ι → Set (β × β)} (K : CompactExhaustion α) (hb : (𝓤 β).HasBasis p V) :
+    HasBasis (𝓤 C(α, β)) (fun i : ℕ × ι ↦ p i.2) fun i ↦
+      {fg | ∀ x ∈ K i.1, (fg.1 x, fg.2 x) ∈ V i.2} :=
+  (UniformOnFun.hasBasis_uniformity_of_covering_of_basis {K | IsCompact K} K.isCompact
+    (Monotone.directed_le K.subset) (fun _ ↦ K.exists_superset_of_isCompact) hb).comap _
+
+theorem _root_.CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity
+    {V : ℕ → Set (β × β)} (K : CompactExhaustion α) (hb : (𝓤 β).HasAntitoneBasis V) :
+    HasAntitoneBasis (𝓤 C(α, β)) fun n ↦ {fg | ∀ x ∈ K n, (fg.1 x, fg.2 x) ∈ V n} :=
+  (UniformOnFun.hasAntitoneBasis_uniformity {K | IsCompact K} K.isCompact
+    K.subset (fun _ ↦ K.exists_superset_of_isCompact) hb).comap _
+
+/-- If `α` is a weakly locally compact σ-compact space
+(e.g., a proper pseudometric space or a compact spaces)
+and the uniformity on `β` is pseudometrizable,
+then the uniformity on `C(α, β)` is pseudometrizable too.
+-/
+instance [WeaklyLocallyCompactSpace α] [SigmaCompactSpace α] [IsCountablyGenerated (𝓤 β)] :
+    IsCountablyGenerated (𝓤 (C(α, β))) :=
+  let ⟨_V, hV⟩ := exists_antitone_basis (𝓤 β)
+  ((CompactExhaustion.choice α).hasAntitoneBasis_compactConvergenceUniformity
+    hV).isCountablyGenerated
+
 variable {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} {f}
 
 /-- Locally uniform convergence implies convergence in the compact-open topology. -/

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

@@ -657,6 +657,53 @@ protected theorem hasBasis_uniformity (h : 𝔖.Nonempty) (h' : DirectedOn (· 
   UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 h h' (𝓤 β).basis_sets
 #align uniform_on_fun.has_basis_uniformity UniformOnFun.hasBasis_uniformity
 
+variable {α β}
+
+/-- Let `t i` be a nonempty directed subfamily of `𝔖`
+such that every `s ∈ 𝔖` is included in some `t i`.
+Let `V` bounded by `p` be a basis of entourages of `β`.
+
+Then `UniformOnFun.gen 𝔖 (t i) (V j)` bounded by `p j` is a basis of entourages of `α →ᵤ[𝔖] β`. -/
+protected theorem hasBasis_uniformity_of_covering_of_basis {ι ι' : Type*} [Nonempty ι]
+    {t : ι → Set α} {p : ι' → Prop} {V : ι' → Set (β × β)} (ht : ∀ i, t i ∈ 𝔖)
+    (hdir : Directed (· ⊆ ·) t) (hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i) (hb : HasBasis (𝓤 β) p V) :
+    (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun i : ι × ι' ↦ p i.2) fun i ↦
+      UniformOnFun.gen 𝔖 (t i.1) (V i.2) := by
+  have hne : 𝔖.Nonempty := (range_nonempty t).mono (range_subset_iff.2 ht)
+  have hd : DirectedOn (· ⊆ ·) 𝔖 := fun s₁ hs₁ s₂ hs₂ ↦ by
+    rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
+    rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
+    exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩
+  refine (UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 hne hd hb).to_hasBasis
+    (fun ⟨s, i'⟩ ⟨hs, hi'⟩ ↦ ?_) fun ⟨i, i'⟩ hi' ↦ ⟨(t i, i'), ⟨ht i, hi'⟩, Subset.rfl⟩
+  rcases hex s hs with ⟨i, hi⟩
+  exact ⟨(i, i'), hi', UniformOnFun.gen_mono hi Subset.rfl⟩
+
+/-- If `t n` is a monotone sequence of sets in `𝔖`
+such that each `s ∈ 𝔖` is included in some `t n`
+and `V n` is an antitone basis of entourages of `β`,
+then `UniformOnFun.gen 𝔖 (t n) (V n)` is an antitone basis of entourages of `α →ᵤ[𝔖] β`. -/
+protected theorem hasAntitoneBasis_uniformity {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
+    {t : ι → Set α} {V : ι → Set (β × β)}
+    (ht : ∀ n, t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n)
+    (hb : HasAntitoneBasis (𝓤 β) V) :
+    (𝓤 (α →ᵤ[𝔖] β)).HasAntitoneBasis fun n ↦ UniformOnFun.gen 𝔖 (t n) (V n) := by
+  have := hb.nonempty
+  refine ⟨(UniformOnFun.hasBasis_uniformity_of_covering_of_basis 𝔖
+    ht hmono.directed_le hex hb.1).to_hasBasis ?_ fun i _ ↦ ⟨(i, i), trivial, Subset.rfl⟩, ?_⟩
+  · rintro ⟨k, l⟩ -
+    rcases directed_of (· ≤ ·) k l with ⟨n, hkn, hln⟩
+    exact ⟨n, trivial, UniformOnFun.gen_mono (hmono hkn) (hb.2 <| hln)⟩
+  · exact fun k l h ↦ UniformOnFun.gen_mono (hmono h) (hb.2 h)
+
+protected theorem isCountablyGenerated_uniformity [IsCountablyGenerated (𝓤 β)] {t : ℕ → Set α}
+    (ht : ∀ n, t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) :
+    IsCountablyGenerated (𝓤 (α →ᵤ[𝔖] β)) :=
+  let ⟨_V, hV⟩ := exists_antitone_basis (𝓤 β)
+  (UniformOnFun.hasAntitoneBasis_uniformity 𝔖 ht hmono hex hV).isCountablyGenerated
+
+variable (α β)
+
 /-- For `f : α →ᵤ[𝔖] β`, where `𝔖 : Set (Set α)` is nonempty and directed, `𝓝 f` admits the
 family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓑` as a filter basis, for any basis
 `𝓑` of `𝓤 β`. -/