Arzela-Ascoli for uniform spaces

Stream: Is there code for X?

[Thomas Browning]

Does mathlib have this statement of Arzela-Ascoli for uniform spaces?
https://en.wikipedia.org/wiki/Arzel%C3%A0%E2%80%93Ascoli_theorem#Functions_on_non-compact_spaces

theorem arzeli_ascoli {X Y : Type*} [TopologicalSpace X] [UniformSpace Y] [CompactSpace Y]
    (H : Set C(X, Y)) (h1 : IsClosed H) (h2 : Equicontinuous ((↑) : H → X → Y)) :
    IsCompact H := sorry

(perhaps with extra hypotheses)

[Vincent Beffara]

Here is some code that @Anatole Dedecker wrote, initially for lean3 but that I adapted for lean4. AFAIK this is not yet in Mathlib?

/-
Copyright (c) 2022 Anatole Dedecker. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anatole Dedecker
-/

import Mathlib.Topology.UniformSpace.Equicontinuity

open Set Filter Uniformity Function UniformConvergence

lemma supr_sUnion [CompleteLattice β] {p : α → β} :
    (⨆ x ∈ ⋃₀ S, p x) = ⨆ (s ∈ S) (x ∈ s), p x := by
  rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']

lemma infi_sUnion [CompleteLattice β] {p : α → β} :
    (⨅ x ∈ ⋃₀ S, p x) = ⨅ (s ∈ S) (x ∈ s), p x := by
  rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']

lemma forall_sUnion {p : α → Prop} :
    (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x := by
  simp_rw [← iInf_Prop_eq, infi_sUnion]

lemma cauchy_of_ne_bot [UniformSpace α] [hl : NeBot l] : Cauchy l ↔ l ×ˢ l ≤ 𝓤 α := by
  simp [Cauchy, hl]

lemma cauchy_pi {α : ι → Type u} [∀ i, UniformSpace (α i)] {l : Filter (∀ i, α i)} [NeBot l] :
    Cauchy l ↔ ∀ i, Cauchy (map (Function.eval i) l) := by
  simp_rw [cauchy_of_ne_bot, prod_map_map_eq, map_le_iff_le_comap, Pi.uniformity, le_iInf_iff]

lemma cauchy_infi {u : ι → UniformSpace α} {l : Filter α} [NeBot l] :
    @Cauchy _ (⨅ i, u i) l ↔ ∀ i, @Cauchy _ (u i) l := by
  have h1 : NeBot l := by assumption
  simp [Cauchy, iInf_uniformity, h1]

lemma cauchy_map_iff_comap {u : UniformSpace β} {f : α → β} {l : Filter α} :
    Cauchy (map f l) ↔ @Cauchy _ (UniformSpace.comap f u) l := by
  simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap, uniformity_comap]
  rfl

variable [TopologicalSpace X] [UniformSpace α] {F : ι → X → α}

lemma theorem1 [CompactSpace X] (hF : Equicontinuous F) :
    (UniformFun.uniformSpace X α).comap F = (Pi.uniformSpace (λ _ => α)).comap F := by
  refine le_antisymm (UniformSpace.comap_mono (le_iff_uniformContinuous_id.mpr UniformFun.uniformContinuous_toFun)) ?_
  change comap _ _ ≤ comap _ _
  simp_rw [Pi.uniformity, Filter.comap_iInf, Filter.comap_comap, Function.comp]
  refine ((UniformFun.hasBasis_uniformity X α).comap (Prod.map F F)).ge_iff.mpr ?_
  intro U hU
  rcases comp_comp_symm_mem_uniformity_sets hU with ⟨V, hV, Vsymm, hVU⟩
  let Ω : X → Set X := λ x => {y | ∀ i, (F i x, F i y) ∈ V}
  rcases CompactSpace.elim_nhds_subcover Ω (λ x => hF x V hV) with ⟨S, Scover⟩
  have : (⋂ s ∈ S, {ij : ι × ι | (F ij.1 s, F ij.2 s) ∈ V}) ⊆ (Prod.map F F) ⁻¹' UniformFun.gen X α U := by
    rintro ⟨i, j⟩ hij x
    rw [mem_iInter₂] at hij
    rcases mem_iUnion₂.mp (Scover.symm.subset $ mem_univ x) with ⟨s, hs, hsx⟩
    exact hVU (prod_mk_mem_compRel (prod_mk_mem_compRel (Vsymm.mk_mem_comm.mp (hsx i)) (hij s hs)) (hsx j))
  exact mem_of_superset (S.iInter_mem_sets.mpr $ λ x _ => mem_iInf_of_mem x $ preimage_mem_comap hV) this

-- TODO: this is too long
lemma theorem1' {𝔖 : Set (Set X)} (h𝔖 : ∀ K ∈ 𝔖, IsCompact K)
    (hF : ∀ K ∈ 𝔖, Equicontinuous ((K.restrict : (X → α) → (K → α)) ∘ F)) :
    (UniformOnFun.uniformSpace X α 𝔖).comap F =
      (⨅ K ∈ 𝔖, ⨅ x ∈ K, ‹UniformSpace α›.comap (eval x)).comap F := by
  rw [UniformOnFun.uniformSpace]
  simp_rw [UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
  refine iInf_congr (λ K => iInf_congr $ λ hK => ?_)
  haveI : CompactSpace K := isCompact_iff_compactSpace.mp (h𝔖 K hK)
  simp_rw [theorem1 (hF K hK), UniformSpace.comap_comap,
            Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, iInf_subtype]
  refine iInf_congr (λ x => iInf_congr $ λ hx => congr_arg _ ?_)
  rw [← UniformSpace.comap_comap]
  exact congr_fun (congr_arg _ rfl) _

lemma theorem1'' {𝔖 : Set (Set X)} (hcover : ⋃₀ 𝔖 = univ) (h𝔖 : ∀ K ∈ 𝔖, IsCompact K)
    (hF : ∀ K ∈ 𝔖, Equicontinuous ((K.restrict : (X → α) → (K → α)) ∘ F)) :
    (UniformOnFun.uniformSpace X α 𝔖).comap F = (Pi.uniformSpace (λ _ => α)).comap F := by
  simp [theorem1' h𝔖 hF, Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, ←infi_sUnion, hcover]

lemma ascoli₀ {𝔖 : Set (Set X)} {F : ι → X →ᵤ[𝔖] α} {l : Filter ι} [NeBot l]
    (h1 : ∀ A ∈ 𝔖, IsCompact A)
    (h2 : ∀ A ∈ 𝔖, Equicontinuous (λ i => Set.restrict A (F i)))
    (h3 : ∀ x ∈ ⋃₀ 𝔖, Cauchy (map (eval x ∘ F) l)) :
    Cauchy (map F l) := by
  have e1 : @Cauchy _ (⨅ K ∈ 𝔖, ⨅ x ∈ K, ‹UniformSpace _›.comap (eval x)) (map F l) := by
    simp_rw [cauchy_infi, ← cauchy_map_iff_comap, ← forall_sUnion]
    exact h3
  rcases e1 with ⟨e2, e3⟩
  refine ⟨e2, ?_⟩
  rw [prod_map_map_eq, map_le_iff_le_comap] at e3 ⊢
  exact e3.trans (theorem1' h1 h2).ge

lemma ascoli {𝔖 : Set (Set X)} {F : ι → X →ᵤ[𝔖] α}
    (h1 : ∀ A ∈ 𝔖, IsCompact A)
    (h2 : ∀ A ∈ 𝔖, Equicontinuous (λ i => Set.restrict A (F i)))
    (h3 : ∀ x ∈ ⋃₀ 𝔖, TotallyBounded (range (λ i => F i x))) :
    TotallyBounded (range F) := by
  simp_rw [totallyBounded_iff_ultrafilter] at h3 ⊢
  intro f hf
  have : F '' univ ∈ f := by rwa [image_univ, ← Ultrafilter.mem_coe, ← le_principal_iff]
  rw [← Ultrafilter.ofComapInfPrincipal_eq_of_map this]
  set g := Ultrafilter.ofComapInfPrincipal this
  apply ascoli₀ h1 h2
  intro x hx
  apply h3 x hx (g.map (eval x ∘ F))
  exact (le_principal_iff.mpr range_mem_map)

[Anatole Dedecker]

Indeed this is not in mathlib yet. The reason is that, although total boundedness is fairly self contained, proving the completeness part to get compactness was easier with some tweaks to the API that I didn’t want to do while the port was going on. I tried an ad-hoc version but ended up never PR-ing it.

[Anatole Dedecker]

But I definitely want to go back to this now that the port is over. Does any of you two need the result in mathlib soon™️ ?

[Anatole Dedecker]

Thanks for porting to Lean4 btw!

[Vincent Beffara]

I would be more interested in a port of !3#18017

[Anatole Dedecker]

Okay, will work on that!

[Vincent Beffara]

But it is not urgent at all

[Thomas Browning]

I hacked together a proof of what I needed at branch#tb_pontryagin_dual. I'll PR it eventually, since I need it for local compactness of the Pontryagin dual. But I don't really understand this subject well. @Anatole Dedecker Are there are any major strategy changes that you would suggest in the proof I wrote?

[Anatole Dedecker]

Well my advice would have been to use my code above, now I feel very bad for not PR-ing it (although in my defense there is a WIP mathlib3 PR on that). I still think that it would be nicer to wait a bit for my version, how quick do you need it?

[Anatole Dedecker]

Now that I'm diving back into this I have the feeling that I missed a big shortcut by relying too much on Bourbaki: the theorem1' in my code above should allow to get directly the compactness result without going through total boundedness and completeness, simply by reducing it to Tychonoff's theorem like Thomas does in his proof. Of course we'll want the completeness results anyways, so maybe the shortcut doesn't actually bring anything, but it still means that I could have provided a stronger statement to Vinvent to begin with...

[Thomas Browning]

Is compactness done (e.g., as stated in my branch)? Not sure whether it's an easy consequence of totally bounded, or requires some additional work.

[Anatole Dedecker]

The way Bourbaki does it is by combining total boundedness and completeness, but as I said there is a shortcut which allows to get compactness directly. They probably don't use it because, well, they have to prove the completeness anyway (and we'll have to do it), but this shortcut means that I should have a ready-for-review PR with almost exactly your statement in a few days (or at least a general statement that easily applies in your case)

[Anatole Dedecker]

If we had to go through completeness it would take more time because that involves a slight refactor of the UniformOnFun file

[Anatole Dedecker]

The idea is to use my theorem1' instead of your suffices

[Anatole Dedecker]

#6693 and #6694 are the two first prerequisite PRs, maybe there will be a third but probably not more

[Thomas Browning]

Oh great, thanks!

[Dean Young]

(deleted)

[Anatole Dedecker]

It took more time than expected (of course...), but I think I've now got #6844 to a pretty good situation. There is still a bit of glue to get to Thomas' precise statement, but it's just a matter of reformulating the content of Topology.UniformSpace.CompactConvergence in terms of the newer docs#UniformOnFun (we should actually rewrite this file, but maybe that's less urgent). @Thomas Browning @Vincent Beffara could you check if the results seem usable enough?
I don't know how much time I will have to take care of this in the near future, so if you want to add some documentation, a module docstring, or simplify some proofs, please have a go!

[Thomas Browning]

Thanks for your help! I'll take a closer look over this next week when I have time.

[Thomas Browning]

@Anatole Dedecker I was wondering how you were planning on getting from your PR to my statement? The issue that I'm having is deducing the inducing assumption present in your formulations from an equicontinuity assumption. I have a painful proof here: https://github.com/leanprover-community/mathlib4/compare/AD_ascoli_part1...tb_ascoli, but I suspect there might be a way to use your work to streamline this a bit?