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?

[Anatole Dedecker]

Sorry for the (very) late answer. I think the reason this is painful is that you shouldn't be using 𝔖 = Set.range Set.singleton (in this case Ascoli theorem is basically useless, you're just using Tychonoff), but rather 𝔖 = {K | IsCompact K}. Then the only thing you have to know is that the natural map from C(X, Y) to X →ᵤ[𝔖] Y is an inducing, which is essentially docs#ContinuousMap.compactOpen_eq_compactConvergence. At some point we should refactor this whole file to use docs#UniformOnFun by the way, but for now it should be easy to get the statement from docs#ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn and docs#UniformOnFun.tendsto_iff_tendstoUniformlyOn

[Anatole Dedecker]

As I said elsewhere, I will have some Lean time during the holiday, and I want to make sure that Ascoli is ready by then so that you don't have to wait for me indefinitely

[Yury G. Kudryashov]

I'll try to refactor that file now.

[Yury G. Kudryashov]

First dependencies: #9257 and #9259

[Thomas Browning]

Anatole Dedecker said:

I think the reason this is painful is that you shouldn't be using 𝔖 = Set.range Set.singleton (in this case Ascoli theorem is basically useless, you're just using Tychonoff), but rather 𝔖 = {K | IsCompact K}.

Thanks, that did the trick!

[Anatole Dedecker]

This is finally ready for review as #6844. Thomas and Vincent, I'm really sorry that you had to wait for so long and suffer from my inability for finish things properly. I think Yury is almost done PR-ing the necessary glue to make that work with docs#ContinuousMap (essentially a ClosedEmbedding statement, we have the embedding part as docs#ContinuousMap.uniformEmbedding_toUniformOnFunIsCompact, and the core of the closed part as docs#UniformOnFun.isClosed_setOf_continuous_of_le), so everything should be ready very soon. Sorry again for the delay.

[Anatole Dedecker]

(I'll admit it, this afternoon's thread about general Fourier theory gave me the final bit of motivation needed to write the module docstring, since I remember you needed that to study the Pontryagin dual)

[Vincent Beffara]

Speaking for myself, I didn't really suffer that much!

[Moritz Doll]

Hey, how far are the results in #6844 from the statement that Thomas wrote in the beginning of this discussion?

[Thomas Browning]

Not far. Here's some glue I wrote a while ago: https://github.com/leanprover-community/mathlib4/compare/AD_ascoli_part1...tb_ascoli

[Moritz Doll]

Cool, thanks. However there is still a compactness assumption that is not in the linked wikipedia article.

[Thomas Browning]

Yes, I'm looking into that. I have a proof without the compactness assumption at #11335, but I'm still figuring out how to deduce it from #6844

[Thomas Browning]

I've dropped the compact assumption, but there's still an unnecessary separation assumption

[Thomas Browning]

@Moritz Doll The extra assumptions should all be gone now.

[Anatole Dedecker]

I realize that the statements I wrote are a bit hard to decipher, but part of the reason is precisely that I had in mind that no one uses docs#UniformOnFun directly, so everything is stated with embeddings and so on. That said, I realize maybe I didn't make the best choices, e.g the Thomas' statement in branch#tb_ascoli doesn't follow from any of my versions because I assume things of the form "$\forall x, \{f(x) | f\in F\}$ is compact" rather than directly assuming compactness of $F$ for the product topology, and thus I need some closedness or separation hypothesis to apply Tykhonov. Do you think such a version should be added? I'm completely open to suggestions here!

[Moritz Doll]

It's not too bad. I've hacked together a version that I am using for the Schwartz space (with unoptimized proof):

variable {ι X α : Type*} [UniformSpace α] [TopologicalSpace X] [WeaklyLocallyCompactSpace X]

theorem arzela_ascoli' [TopologicalSpace ι] [T2Space α]
    {s : Set C(X, α)}
    (s_eqcont : ∀ (K : Set X) (_hK : IsCompact K), EquicontinuousOn (((↑) : s → X → α)) K)
    (s_pointwiseCompact : ∀ (K : Set X) (hK : IsCompact K),
      ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ f ∈ s, f x ∈ Q) :
    IsCompact (closure s) := by
  apply ArzelaAscoli.isCompact_closure_of_closedEmbedding (𝔖 := {K : Set X | IsCompact K}) (α := α)
    (by simp) _ s_eqcont s_pointwiseCompact
  rw [closedEmbedding_iff]
  constructor
  · exact ContinuousMap.uniformEmbedding_toUniformOnFunIsCompact.embedding
  · rw [isClosed_iff_forall_filter]
    intro f u v hu huf
    rw [← Filter.tendsto_id'] at huf
    rw [UniformOnFun.tendsto_iff_tendstoUniformlyOn] at huf
    refine ⟨⟨f, ?_⟩, rfl⟩
    rw [continuous_iff_continuousAt]
    intro x
    rcases WeaklyLocallyCompactSpace.exists_compact_mem_nhds x with ⟨K, hK1, hK2⟩
    refine ((huf K hK1).continuousOn (Filter.le_principal_iff.mp ?_)).continuousAt hK2
    apply hu.trans
    simp only [Function.comp_apply, id_eq, Filter.le_principal_iff, Filter.mem_principal]
    intro y ⟨y0, hy⟩
    apply Continuous.continuousOn
    convert y0.continuous
    rw [← hy]
    simp only [Function.comp_apply, UniformOnFun.toFun_ofFun]

[Anatole Dedecker]

This is more the kind of version I was expecting. The closed part will be in Mathlib soon, Yury is working on it, so you'll be able to remove the last dot.

[Anatole Dedecker]

That said I've just realized there is a small catch. The fact that C(X, Y) has closed range in X →ᵤ[𝔖] α does require some form of local compactness (actually compact generation), but this is not the case for equicontinuous subsets since there even a pointwise limit of continuous functions is continuous. So we should add something like this:

open ContinuousMap in
theorem Equicontinuous.closedEmbedding_toUniformOnFunIsCompact {X : Type*}
    [TopologicalSpace X] {φ : X → C(α, β)} (hφ₁ : Equicontinuous ((↑) ∘ φ))
    (hφ₂ : ClosedEmbedding φ) :
    ClosedEmbedding (toUniformOnFunIsCompact ∘ φ : X → α →ᵤ[{K | IsCompact K}] β) where
  toEmbedding := uniformEmbedding_toUniformOnFunIsCompact.embedding.comp hφ₂.toEmbedding
  closed_range := by
    rw [isClosed_iff_forall_filter]
    intro f ℱ hℱ hℱφ hℱf
    set 𝒢 : Filter X := comap (toUniformOnFunIsCompact ∘ φ) ℱ
    have hℱ𝒢 : map (toUniformOnFunIsCompact ∘ φ) 𝒢 = ℱ :=
      map_comap_of_mem (hℱφ <| mem_principal_self _)
    have : NeBot 𝒢 := by rwa [← hℱ𝒢, map_neBot_iff] at hℱ
    have h𝒢f : Tendsto (toUniformOnFunIsCompact ∘ φ) 𝒢 (𝓝 f) := by
      rwa [← hℱ𝒢, ← Tendsto] at hℱf
    have : Tendsto ((↑) ∘ φ) 𝒢 (𝓝 <| UniformOnFun.toFun {K | IsCompact K} f) := by
      refine UniformOnFun.uniformContinuous_toFun ?_ |>.continuous.tendsto _ |>.comp h𝒢f
      exact sUnion_eq_univ_iff.mpr fun x ↦ ⟨{x}, isCompact_singleton, rfl⟩
    have hf : Continuous f := this.continuous_of_equicontinuous hφ₁
    have : ⟨f, hf⟩ ∈ range φ := hφ₂.closed_range.mem_of_tendsto
      (uniformEmbedding_toUniformOnFunIsCompact.embedding.tendsto_nhds_iff.mpr <| by exact h𝒢f)
      (eventually_of_forall fun _ ↦ mem_range_self _)
    rw [range_comp]
    exact ⟨⟨f, hf⟩, this, rfl⟩

Then unfortunately one can no longer apply directly isCompact_closure_of_closedEmbedding, but we can mimick its proof:

theorem arzela_ascoli {X Y : Type*} [TopologicalSpace X] [UniformSpace Y]
    [T2Space Y] (s : Set C(X, Y))
    (s_pointwiseCompact : ∀ (K : Set X) (hK : IsCompact K),
      ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ f ∈ s, f x ∈ Q)
    (S_eqcont : Equicontinuous (((↑) : s → X → Y))) :
    IsCompact (closure s) := by
  rw [isCompact_iff_compactSpace]
  have cls_eqcont := S_eqcont.closure' ContinuousMap.continuous_coe
  have cls_pointwiseCompact : ∀ K, IsCompact K → ∀ x ∈ K,
      ∃ Q, IsCompact Q ∧ ∀ f ∈ closure s, f x ∈ Q :=
    fun K hK x hx ↦ (s_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, closure_minimal hQ.2 <|
      hQ.1.isClosed.preimage <| ContinuousMap.continuous_eval_const _⟩
  refine ArzelaAscoli.compactSpace_of_closedEmbedding (fun _ ↦ id)
    (cls_eqcont.closedEmbedding_toUniformOnFunIsCompact
      (isClosed_closure).closedEmbedding_subtype_val)
    (fun _ _ ↦ cls_eqcont.equicontinuousOn _)
    (fun K hK x hx ↦ (cls_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, by simpa using hQ.2⟩)

[Anatole Dedecker]

I’ll think about what’s the best API design here, I only realized recently that the natural map from continuous functions was not always a closed embedding…

[Anatole Dedecker]

Note also that for this to work you really need to assume equicontinuity everywhere, not on each compact (and indeed this is what is assumed in Bourbaki, I should have thought about why they don’t use the weaker assumption…)

[Anatole Dedecker]

@Vincent Beffara Could you remind me what setup do you need this for exactly? I'd like to have an idea of what is actually useful and what is not. I'm pretty sure you're dealing with functions not continuous on the whole space so using docs#ContinuousMap is an option, is that right?

[Vincent Beffara]

The results I need are this:

def compacts (U : Set ℂ) : Set (Set ℂ) := {K | K ⊆ U ∧ IsCompact K}
instance : CompleteSpace (ℂ →ᵤ[compacts U] ℂ) := by sorry

and Montel's theorem here: https://github.com/vbeffara/RMT4/blob/main/RMT4/montel.lean (stated for {F : ι → ℂ →ᵤ[compacts U] ℂ})

I probably should rebase my project on top of your PR and see what happens. Maybe using ContinuousMap instead of ContinuousOn makes sense (though I vaguely remember at some point that Patrick was warning me agains it because of all the coercions).

[Anatole Dedecker]

Note that I now go straight towards compactness (assuming compactness on the fibers), at least for that first PR, but it shouldn’t make your life any harder since total boundedness and relative compactness are the same in $\mathbb{C}$. So maybe you don’t need completeness anymore, but I think we will have it soon anyways

[Vincent Beffara]

theorem RMT (h1 : IsOpen U) (h2 : IsConnected U) (h3 : U ≠ univ) (h4 : has_primitives U) :
    ∃ f : ℂ → ℂ, (DifferentiableOn ℂ f U) ∧ (InjOn f U) ∧ (f '' U = ball 0 1) := by ...

#print axioms RMT
-> 'RMT' depends on axioms: [propext, Classical.choice, Quot.sound]

Thanks! :tada: