Montel's theorem

Stream: maths

[Vincent Beffara]

I would like to have a go at proving Montel's theorem, which in my head is this:

theorem montel {U : set ℂ} {F : ℕ → ℂ → ℂ}
  (hU : is_open U)
  (hF1 : ∀ n, differentiable_on ℂ (F n) U)
  (hF2 : ∀ K ⊆ U, is_compact K → ∃ M : ℝ, ∀ n, ∀ z ∈ K, ‖F n z‖ ≤ M)
  :
  ∃ (φ : ℕ → ℕ) (f : ℂ → ℂ), tendsto φ at_top at_top ∧
    tendsto_locally_uniformly_on (λ n, F (φ n)) f at_top U

On paper I would say something along the lines of "up to a diagonal extraction it is enough to work on a fixed compact set, and on a compact set this is just a simple application of Arzela-Ascoli with a bound on the modulus of continuity obtained by Cauchy's integral formula for the derivative". But that is not very formal... so I need some advice.

• probably the right mathlib-ish statement at the right level of generality would be stated in terms of various filters rather than on sequences, but my experience in this domain is not good enough to figure it out exactly. What would the appropriate statement be? [As far as I am concerned, the sequential statement is enough for what I want to do with it.]
• it feels natural to use docs#bounded_continuous_function.arzela_ascoli but this is written in terms of bounded_continuous_function while all of the complex analysis in mathlib is written in terms of differentiable_on for f : \C \to \C and going back and forth between them is a bit painful.

So in fact I am tempted to write the more general version of Arzela-Ascoli directly under locally uniform assumptions on an open set and derive docs#bounded_continuous_function.arzela_ascoli from it, rather than the other way. Does that sound like a reasonable plan, or would it be better to go the other way?

[Sebastien Gouezel]

Not really answering your question, but #16467 looks relevant.

[Sebastien Gouezel]

I think it would definitely make sense to have versions of Arzela-Ascoli for the topology of uniform convergence on some subset (this topology is defined in the file topology/uniform_space/uniform_convergence_topology), and also for the topology of locally uniform convergence on a family of subsets (but I don't think we have this one, although tendsto_locally_uniformly is defined). The current Arzela-Ascoli predates all these, so it is certainly improvable!

I agree with you that proving a general statement for uniform convergence or locally uniform convergence and then deducing the current Arzela-Ascoli version from it is probably the right thing to do, because the other direction feels less natural.

[Sebastien Gouezel]

@Anatole Dedecker would probably have good ideas on what would be the best path here.

[Sebastien Gouezel]

In fact we also have the topology of uniform convergence on a family of subsets, on the type denoted with α →ᵤ[𝔖] β(where 𝔖 is the set of sets where one requires uniform convergence), so the most general version of Arzela-Ascoli should probably be formulated for this one.

[Vincent Beffara]

Thanks for the pointers! In fact it might be a fair guess that @Anatole Dedecker is actually working on that, because the whole α →ᵤ[𝔖] β type alias construction is following quite closely chapter X of Bourbaki TG and Ascoli is just a few pages further. IIUC the statements from there could be stated something like this:

variables {α β ι : Type*} {𝔖 : set (set α)} {F : ι → (α →ᵤ[𝔖] β)}

theorem ascoli [topological_space α] [uniform_space β]
  (h1 : ⋃₀ 𝔖 = set.univ)
  (h2 : ∀ A ∈ 𝔖, is_compact A)
  (h3 : ∀ A ∈ 𝔖, equicontinuous (λ i, set.restrict A (F i)))
  (h4 : ∀ x, totally_bounded (range (λ i, F i x))) :
  totally_bounded (range F) := sorry

theorem ascoli' [uniform_space α] [uniform_space β]
  (h1 : ⋃₀ 𝔖 = set.univ)
  (h2 : ∀ A ∈ 𝔖, totally_bounded A)
  (h3 : ∀ A ∈ 𝔖, uniform_equicontinuous (λ i, set.restrict A (F i)))
  (h4 : ∀ x, totally_bounded (range (λ i, F i x))) :
  totally_bounded (range F) := sorry

although a potentially useful generalization would assume something like along some filter on the index type, on any A the functions are eventually equicontinuous (but then I'm not sure what the conclusion should be).

[Patrick Massot]

Anatole has his end of term exams next week so you cannot expect answers soon. But I'm sure he will easily handle all that later.

[Vincent Beffara]

Ah OK. I could give it a try myself but it's probably more natural if he does it...

[Ruben Van de Velde]

As a former student, isn't that the time of year when you're most easily distracted by non-exam things? But maybe Anatole is a better student than I was :sweat_smile:

[Vincent Beffara]

I'm half expecting 500 lines of code from him at 2AM with a comment like "now I have to study for my exams" :grinning_face_with_smiling_eyes:

[Patrick Massot]

I am in charge of the program where Anatole is studying...

[Anatole Dedecker]

Sorry for the delay! I am indeed studying for my exams, so as Patrick said I am not going to have much time to devote to Lean until the end of the week, and much of this time is dedicated to keeping my PRs kind-of up-to-date, but the good news is that I won't have anything to do during the holidays, so I'll have plenty of Lean time then. But I wanted to give some answers already.
So indeed, since #16467 is merged, we now have equicontinuity, as well as the topologies of uniform convergence on the whole set and on some families of subsets. When I made the equicontinuity PR I decided not to completely refactor the current Arzela Ascoli (although I did some low-hanging steps, like equicontinuity being preserved by closure), because my main target was (and still is) the general Banach Steinhaus theorem, but I definitely wanted to go back to it if no one had done it earlier. So if you're okay to wait a bit and don't want to do it yourself, I would be happy to work on that in priority during the holidays!
Another thing that has been in my mind is to adapt the uniform convergence topologies to our new docs#tendsto_uniformly_on_filter. This would allow to truly have the topology of local uniform convergence without any trick like "let's just say we mean uniform convergence on compact sets because we are working on a locally compact space". I don't think this is in Bourbaki, but AFAIK this should be pretty straightforward.

[Anatole Dedecker]

Ruben Van de Velde said:

As a former student, isn't that the time of year when you're most easily distracted by non-exam things? But maybe Anatole is a better student than I was :sweat_smile:

Actually I used to do that a lot too, but for some reason I'm not falling into that this year. I guess one reason is that basically all of my courses are things I really like now, so when I'm bored of one subject, switching to anothere is just as tempting as a distraction as opening Lean or other things like that.

[Yaël Dillies]

Anatole Dedecker said:

when I'm bored of one subject, switching to another is just as tempting as a distraction as opening Lean or other things like that.

The Yaël is willing but the mind is weak :speechless:

[Vincent Beffara]

Hi, so I had a look at the type aliases for convergences, and got a bit lost. In particular, I didn't find a satisfactory way of stating that "this and that uniform space structures induce the same uniformity on this particular set of functions" (Lean kept reading what I wrote as a rfl in disguise because it saw a bit too much through type aliases.)

OTOH I am now more motivated to try, because Montel's theorem is the last step missing for the Riemann mapping theorem: with it, the proof is complete in the sense that for every connected strict open set in the complex plane on which every holomorphic function has a primitive, there is a bi-holomorphic bijection with the unit disk. A lot of the proof will likely have to be rewritten once contour integrals (and meromorphic functions) are in mathlib ... and given the state of the code, all that will likely have to happen after the flood

[Anatole Dedecker]

Sorry for the delay, now I should be able to answer much more quickly :grinning_face_with_smiling_eyes:

So indeed one downside of switching to type aliases is that you have to be careful about when to abuse defeq and when not. Note however that you can still refer to the uniform structure itself as docs#uniform_fun.uniform_space, so the first "solution" is to embrace the @s and do everything by hand.
If we want to keep the type aliases, we have to go to the other extreme and write docs#uniform_equiv instead of equalities of uniform structure. But here I would need more information about your specific use case (in particular, when you say "a set of functions" do you mean some type or really some subset of X -> Y?)

[Anatole Dedecker]

Okay so I started looking into Bourbaki's proof and I see where you have to do this kind of painful things. I think here there is no way to avoid a bunch of @s, but it shouldn't leak out too much so that should be fine :fingers_crossed:

[Anatole Dedecker]

Here is a first sorry-free version!

import topology.uniform_space.equicontinuity

open set filter uniform_space function
open_locale filter topological_space uniform_convergence uniformity

lemma cauchy_of_ne_bot {α : Type*} [uniform_space α] {l : filter α} [hl : l.ne_bot] :
  cauchy l ↔ l ×ᶠ l ≤ 𝓤 α :=
by simp only [cauchy, hl, true_and]

lemma cauchy_pi {ι : Type*} {α : ι → Type*} [Π i, uniform_space (α i)]
  {l : filter (Π i, α i)} [l.ne_bot] : cauchy l ↔ ∀ i, cauchy (map (eval i) l) :=
by simp_rw [cauchy_of_ne_bot, prod_map_map_eq, map_le_iff_le_comap, Pi.uniformity, le_infi_iff]

variables {ι X α β : Type*} [topological_space X] [uniform_space α] [uniform_space β]
  {F : ι → X → α} {G : ι → β → α}

lemma theorem1 [compact_space X] (hF : equicontinuous F) :
  (uniform_fun.uniform_space X α).comap F =
  (Pi.uniform_space (λ _, α)).comap F :=
begin
  refine le_antisymm (uniform_space.comap_mono $ le_iff_uniform_continuous_id.mpr $
    uniform_fun.uniform_continuous_to_fun) _,
  change comap _ (𝓤 _) ≤ comap _ (𝓤 _),
  simp_rw [Pi.uniformity, filter.comap_infi, filter.comap_comap, function.comp],
  refine ((uniform_fun.has_basis_uniformity X α).comap (prod.map F F)).ge_iff.mpr _,
  intros 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 compact_space.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) ⁻¹' uniform_fun.gen X α U,
  { rintro ⟨i, j⟩ hij x,
    rw mem_Inter₂ at hij,
    rcases mem_Union₂.mp (Scover.symm.subset $ mem_univ x) with ⟨s, hs, hsx⟩,
    exact hVU (prod_mk_mem_comp_rel (prod_mk_mem_comp_rel
      (Vsymm.mk_mem_comm.mp (hsx i)) (hij s hs)) (hsx j)) },
  exact mem_of_superset
    (S.Inter_mem_sets.mpr $ λ x hxS, mem_infi_of_mem x $ preimage_mem_comap hV) this,
end

-- TODO: this is too long
lemma theorem1' {𝔖 : set (set X)} (h1 : ⋃₀ 𝔖 = univ) (h2 : ∀ K ∈ 𝔖, is_compact K)
  (hF : ∀ K ∈ 𝔖, equicontinuous ((K.restrict : (X → α) → (K → α)) ∘ F)) :
  (uniform_on_fun.uniform_space X α 𝔖).comap F = (Pi.uniform_space (λ _, α)).comap F :=
begin
  refine le_antisymm (uniform_space.comap_mono $ le_iff_uniform_continuous_id.mpr $
    uniform_on_fun.uniform_continuous_to_fun h1) _,
  rw [uniform_on_fun.uniform_space],
  simp_rw [uniform_space.comap_infi, le_infi₂_iff, ← uniform_space.comap_comap],
  intros K hK,
  haveI : compact_space K := is_compact_iff_compact_space.mp (h2 K hK),
  rw [theorem1 (hF K hK), @uniform_space.comap_comap _ _ _ _ F],
  refine uniform_space.comap_mono _,
  rw [← uniform_continuous_iff, uniform_continuous_pi],
  exact λ i, Pi.uniform_continuous_proj _ i
end

lemma ascoli₀ {𝔖 : set (set X)} {F : ι → X →ᵤ[𝔖] α} {l : filter ι} [l.ne_bot]
  (h1 : ⋃₀ 𝔖 = set.univ)
  (h2 : ∀ A ∈ 𝔖, is_compact A)
  (h3 : ∀ A ∈ 𝔖, equicontinuous (λ i, set.restrict A (F i)))
  (h4 : ∀ x, cauchy (map (eval x ∘ F) l)) :
  cauchy (map F l) :=
begin
  change ∀ x, cauchy (map (eval x) (map F l)) at h4,
  rw ← cauchy_pi at h4,
  rw [cauchy_of_ne_bot, prod_map_map_eq, map_le_iff_le_comap] at ⊢ h4,
  exact h4.trans (theorem1' h1 h2 h3).ge
end

lemma ascoli {𝔖 : set (set X)} {F : ι → X →ᵤ[𝔖] α}
  (h1 : ⋃₀ 𝔖 = set.univ)
  (h2 : ∀ A ∈ 𝔖, is_compact A)
  (h3 : ∀ A ∈ 𝔖, equicontinuous (λ i, set.restrict A (F i)))
  (h4 : ∀ x, totally_bounded (range (λ i, F i x))) :
  totally_bounded (range F) :=
begin
  simp_rw totally_bounded_iff_ultrafilter at ⊢ h4,
  intros f hf,
  have : F '' univ ∈ f,
  { rwa [image_univ, ← ultrafilter.mem_coe, ← le_principal_iff] },
  rw ← ultrafilter.of_comap_inf_principal_eq_of_map this,
  set g := ultrafilter.of_comap_inf_principal this,
  refine ascoli₀ h1 h2 h3 (λ x, h4 x (g.map (eval x ∘ F)) $ le_principal_iff.mpr $ range_mem_map)
end

[Kevin Buzzard]

Nice!

[Anatole Dedecker]

In particular I'm quite happy with the intermediate ascoli₀ in the above, because I can think of a lot of cases where being able to work directly with indexed sequences/families would be nice while having to deal with totally_bounded (range ...) (or even is_compact (range ...)) would be annoying.

[Anatole Dedecker]

And this also suggests a way to make an eventually statement: the natural thing to try would be replacing h3 by ∀ A ∈ 𝔖, ∀ᶠ (B : set ι) in l.small_sets, equicontinuous (λ i : B, set.restrict A (F i)) (or ∀ᶠ (B : set ι) in l.small_sets, ∀ A ∈ 𝔖, equicontinuous (λ i : B, set.restrict A (F i))) in ascoli₀

[Vincent Beffara]

That's really nice! (And I was far from knowing the current API to be able to reach such a proof in finite time.)

Actually, do we really need assumption h1? (I mean, if then h4 says ∀ x ∈ ⋃₀ 𝔖.) Removing it would help in applications where assumptions are in terms of continuous_on. E.g.

example {F : ι → X →ᵤ[{∅}] α} {l : filter ι} [l.ne_bot] : cauchy (map F l) :=
begin
  have := uniform_on_fun.has_basis_uniformity X α {∅} (by simp) sorry,
  apply this.cauchy_iff.2,
  simp [filter.map_ne_bot],
  rintro a b rfl hb,
  refine ⟨univ, _⟩,
  simp [uniform_on_fun.gen],
end

[Anatole Dedecker]

Actually, do we really need assumption h1? (I mean, if then h4 says ∀ x ∈ ⋃₀ 𝔖)

That should definitely be doable, but the biggest question is (as usual) what's easier between doing the general version first or deducing it from the particular one. I'll give it a try.

Removing it would help in applications where assumptions are in terms of continuous_on

That makes me realize that maybe we want equicontinuous_on already. I discussed that with Sébastien on the equicontinuity PR and decided that we would add it when needed. You probably have way more uses of Ascoli in mind than I do, what do you think about this?

And I was far from knowing the current API to be able to reach such a proof in finite time.

To be honest the uniform_space API is really tricky to get right imo. The two main reasons I see are:

• unintuitive lemma names (e.g I never remember the name of docs#comp_comp_symm_mem_uniformity_sets)
• having to switch all the time between uniformity, uniform_space.core.uniformity and the raw uniform_space, because each of them have associated lemmas (see e.g the difference between the definition of docs#uniform_continuous and docs#uniform_continuous_iff)

[Vincent Beffara]

Actually, do we really need assumption h1? (I mean, if then h4 says ∀ x ∈ ⋃₀ 𝔖)

That should definitely be doable, but the biggest question is (as usual) what's easier between doing the general version first or deducing it from the particular one. I'll give it a try.

In fact tracing the API around it, there are many places where 𝔖 being nonempty is assumed, where as far as I understood it it should work without the assumption (though admittedly the empty case is a bit boring). It would be optimal to have neither the nonempty nor the covering assumption.

Removing it would help in applications where assumptions are in terms of continuous_on

That makes me realize that maybe we want equicontinuous_on already. I discussed that with Sébastien on the equicontinuity PR and decided that we would add it when needed. You probably have way more uses of Ascoli in mind than I do, what do you think about this?

The main use case that I have for the moment is Montel, so uniformly bounded families of holomorphic functions on a domain of the complex plane. So I care more about 𝔖 = {K \ss U | is_compact K} than about an additional definition.

[Anatole Dedecker]

So actually removing h1 is not hard at all, but making h4 only require Cauchyness for elements of ⋃₀ 𝔖 is much more annoying...

[Anatole Dedecker]

In fact tracing the API around it, there are many places where 𝔖 being nonempty is assumed, where as far as I understood it it should work without the assumption (though admittedly the empty case is a bit boring). It would be optimal to have neither the nonempty nor the covering assumption.

If you're talking about the uniform_on_fun API, the thing is that docs#uniform_on_fun.has_basis_uniformity_of_basis does require nonemptyness and directedness (otherwise it isn't a filter basis to begin with!). The point where we get too strong assumptions is when I want to use this lemma to prove facts that don't depend directly on 𝔖. The reason is that I could replace 𝔖 by its generated noncovering bornology, which is automatically nonempty and directed, without changing the topology. The reason we don't have that yet is that we don't have noncovering bornologies (because of docs#bornology.le_cofinite) so this is really annoying to even state.
That said, I'm not sure this is too relevant here, because the covering condition is needed anyway if we want to compare uniform convergence and pointwise convergence: if the sets on which you have uniform convergence do not cover the space, you can't hope to have pointwise convergence

[Dean Young]

(deleted)

[Kevin Buzzard]

(deleted)

[Anatole Dedecker]

What do you think is the most useful as an hypothesis, ∀ x ∈ ⋃₀ 𝔖, cauchy (map (eval x ∘ F) l) or ∀ K ∈ 𝔖, ∀ x ∈ K, cauchy (map (eval x ∘ F) l)?

[Kevin Buzzard]

My guess is the second one?

[Anatole Dedecker]

I just pushed a fully relative version at #17975. It was a bit annoying because I can no longer say that ∀ x ∈ ⋃₀ 𝔖, cauchy (map (eval x ∘ F) l) means being Cauchy for the product, so I have to go back to bare infimums and pullbacks, but the end result is clearly better

[Anatole Dedecker]

Kevin Buzzard said:

My guess is the second one?

I would say the same, but since Vincent has a concrete application in mind I'd like to make sure everything works in his case

[Anatole Dedecker]

I will also add

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

anyway

[Vincent Beffara]

They feel the same to me - perhaps option 2 does indeed make things a bit more modular

[Yaël Dillies]

Noncovering bornologies are exactly filters, right? Or is there a difference?

[Anatole Dedecker]

Yes but that should be an implementation detail hidden from the user, because having complements everywhere is super annoying

[Vincent Beffara]

OK so with the relative version I can now prove this:

def compacts (U : set ℂ) : set (set ℂ) := {K | K ⊆ U ∧ is_compact K}

variables {ι : Type*} {U K : set ℂ} {F : ι → ℂ →ᵤ[compacts U] ℂ}

def uniformly_bounded_on (F : ι → ℂ → ℂ) (U : set ℂ) : Prop :=
  ∀ K ∈ compacts U, ∃ M > 0, ∀ z ∈ K, range (function.eval z ∘ F) ⊆ closed_ball 0 M

theorem montel (hU : is_open U) (h1 : uniformly_bounded_on F U)
  (h2 : ∀ i, differentiable_on ℂ (F i) U) :
  totally_bounded (range F)

(the definition of uniformly_bounded_on is not spelt the right way, it just minimized the local pain at some point in the proof ...)

[Yaël Dillies]

Anatole Dedecker said:

Yes but that should be an implementation detail hidden from the user, because having complements everywhere is super annoying

Do you mean you need docs#order.ideal?

[Yaël Dillies]

In that case let me tell you that the API is a bit bad, but that I have a refactor on a branch that improves it greatly

[Yaël Dillies]

Then the refactor would redefine docs#filter in terms of docs#pfilter so that we can start porting filter lemmas to pfilter and dualise them to ideal.

[Anatole Dedecker]

Yaël Dillies said:

Then the refactor would redefine docs#filter in terms of docs#pfilter so that we can start porting filter lemmas to pfilter and dualise them to ideal.

Hasn't this been dicussed a few times before, with the conclusion that we would lose a lot of nice definitional equalities in the case of filters on sets?

[Anatole Dedecker]

Yaël Dillies said:

Anatole Dedecker said:

Yes but that should be an implementation detail hidden from the user, because having complements everywhere is super annoying

Do you mean you need docs#order.ideal?

Essentially yes, in my mind bornology would have been to docs#order.ideal what docs#filter is to docs#pfilter

[Anatole Dedecker]

To be honest I still don't see any reason to have the current restriction in the definition of bornology, and not just have it as a typeclass, apart from being slightly more consistent with the current litterature. In the context of topological vector spaces, this basically corresponds to restricting to T2 spaces!

[Anatole Dedecker]

But there are other changes I want to discuss about docs#bornology, and we should wait for Lean4 before changing things here, especially since it appears quite low in the import tree (docs#metric_space depends on it!)

[Anatole Dedecker]

Vincent Beffara said:

OK so with the relative version I can now prove this:

def compacts (U : set ℂ) : set (set ℂ) := {K | K ⊆ U ∧ is_compact K}

variables {ι : Type*} {U K : set ℂ} {F : ι → ℂ →ᵤ[compacts U] ℂ}

def uniformly_bounded_on (F : ι → ℂ → ℂ) (U : set ℂ) : Prop :=
  ∀ K ∈ compacts U, ∃ M > 0, ∀ z ∈ K, range (function.eval z ∘ F) ⊆ closed_ball 0 M

theorem montel (hU : is_open U) (h1 : uniformly_bounded_on F U)
  (h2 : ∀ i, differentiable_on ℂ (F i) U) :
  totally_bounded (range F)

(the definition of uniformly_bounded_on is not spelt the right way, it just minimized the local pain at some point in the proof ...)

This is nice! Just out of curiosity, did you try getting your original statement (with the subsequence) directy from the cauchy statement? I'm not sure this is the optimal road at all, but I feel like this is something that should be easy but isn't due to lack of API (I can't even find any links between docs#cluster_pt and actual subsequences!), so it would be nice to at least make sure we can make it work

[Anatole Dedecker]

Side note: in an ideal world, we would have a nice way to show that your uniformly_bounded_on def is just docs#bornology.is_bounded for the Von Neuman bornology on ℂ →ᵤ[compacts U] ℂ!

[Antoine Chambert-Loir]

Anatole Dedecker said:

What do you think is the most useful as an hypothesis, ∀ x ∈ ⋃₀ 𝔖, cauchy (map (eval x ∘ F) l) or ∀ K ∈ 𝔖, ∀ x ∈ K, cauchy (map (eval x ∘ F) l)?

Shouldn't there be a lemma that passes from one to another, possibly for other properties than cauchy _ ?

[Anatole Dedecker]

I will add this indeed:

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

But there is still a point to be made that one is more natural to use because it doesn't involve any existential, so if everyone ends up rewriting to one form let's just use it directly.

[Anatole Dedecker]

(infi_sUnion doesn't exist yet either outside of the draft #17975)

[Anatole Dedecker]

Just out of curiosity, did you try getting your original statement (with the subsequence) directy from the cauchy statement? I'm not sure this is the optimal road at all, but I feel like this is something that should be easy but isn't due to lack of API (I can't even find any links between docs#cluster_pt and actual subsequences!), so it would be nice to at least make sure we can make it work

I spent a bit of time trying to do that and I came to the conclusion that 1) my explanation wasn't clear and 2) what I had in mind cannot work. Basically, I was trying to say "instead of assuming total boundedness (which means that any ultrafilter is cauchy), why not just assume that F has pointwise cluster points, and then we should be able to deduce a cluster point for the whole sequence of functions in the same way that we prove that pointwise totally-bounded implies uniformly-totally-bounded". But that cannot work, essentially because "I have a converging subsequence" and "all my subsequences have a converging subsequence" are not the same thing

[Anatole Dedecker]

So I guess now I have to prove that X →ᵤ[𝔖] α is complete when α is and then Vincent will be able to get what he wants, modulo some API about docs#totally_bounded

[Anatole Dedecker]

I have to prove that X →ᵤ[𝔖] α is complete when α is

Actually we already have that for the ad-hoc docs#tendsto_uniformly_on. We really need to make more bridges between these, and in particular I have to backport our new docs#tendsto_uniformly_on_filter. Presumably one could get rid of the predicates and use docs#uniform_fun and variants of it, but I'm not sure about that.

[Yaël Dillies]

Anatole Dedecker said:

Hasn't this been dicussed a few times before, with the conclusion that we would lose a lot of nice definitional equalities in the case of filters on sets?

We can keep any filter definition and show its equivalence with a pfilter one if we really care about defeq.

[Vincent Beffara]

I don't think using a sequence is the mathlib-appropriate way to do it, I was just following the proof I have on paper and found docs#exists_seq_tendsto_Sup and went with it. I would expect a smoother way to replace maximizing sequences would be to state (nhds_within (supr f) (range f)).ne_bot and use comap but I found nothing to do that in mathlib

[Vincent Beffara]

Ah, docs#is_lub.nhds_within_ne_bot

[Anatole Dedecker]

I don't think using a sequence is the mathlib-appropriate way to do it

Oh indeed I talked about sequences because the problem is easier to see, but of course I tried it with filters from the beginning. You can replace "sequence" by "fillter and "subsequence" by "finer ultrafilter" in what I said

[Anatole Dedecker]

Sorry, I don't understand how order gets involved into any of that :thinking:

[Anatole Dedecker]

The way I thought you wanted to do it is getting relative compactness of the range (from a variant of Ascoli) and then use docs#is_compact.tendsto_subseq

[Anatole Dedecker]

Anatole Dedecker said:

So I guess now I have to prove that X →ᵤ[𝔖] α is complete when α is and then Vincent will be able to get what he wants, modulo some API about docs#totally_bounded

Actually I should have read Bourbaki better, I don't even need it to get relative compactness from total boundedness here, because we know that in our setup we might as well work with docs#Pi.uniform_space (and we have docs#Pi.complete_space)

[Vincent Beffara]

Quick update: if you can show complete_space (ℂ →ᵤ[compacts U] ℂ), or if you can show compactness given total boundedness and closedness in ℂ →ᵤ[compacts U] ℂ, then I can now complete the proof of

def has_primitives (U : set ℂ) : Prop :=
∀ f : ℂ → ℂ, differentiable_on ℂ f U → ∃ g : ℂ → ℂ, differentiable_on ℂ g U ∧ eq_on (deriv g) f U

theorem RMT (h1 : is_open U) (h2 : is_connected U) (h3 : U ≠ univ) (h4 : has_primitives U) :
  ∃ f : ℂ → ℂ, (differentiable_on ℂ f U) ∧ (inj_on f U) ∧ (f '' U = ball 0 1)

[Kalle Kytölä]

This is absolutely great! I hope the Riemann Mapping Theorem makes it to mathlib soon. :tada:

[Anatole Dedecker]

(For anyone wondering, I am working on the missing bit)

[Anatole Dedecker]

And here it is: #18017

[Anatole Dedecker]

This is still a mess (especially, the last few proofs, I just wanted to have them done for now!), and in particular I have to think of how to better integrate this with docs#uniform_cauchy_seq_on_filter.tendsto_uniformly_on_filter_of_tendsto
I'm pretty sure I can't use this last one directly because an infimum of complete spaces has no good reason to be complete, but it's essentially the same argument over and over again of going back to docs#Pi.complete_space. So I implemented Bourbaki's machinery to deal with this, which is this lemma

[Anatole Dedecker]

At the moment it really looks like a more direct proof would have been shorter, but this should allow me to minimize some assumptions on Ascoli too (there is one version which gives compactness without assuming completeness of the codomain)