Zulip Chat Archive

Stream: maths

Topic: Montel's theorem


Vincent Beffara (Dec 06 2022 at 09:40):

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 (Dec 06 2022 at 09:59):

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

Sebastien Gouezel (Dec 06 2022 at 10:10):

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 (Dec 06 2022 at 10:11):

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

Sebastien Gouezel (Dec 06 2022 at 10:19):

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 (Dec 07 2022 at 10:36):

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 (Dec 07 2022 at 12:09):

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 (Dec 07 2022 at 12:14):

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

Ruben Van de Velde (Dec 07 2022 at 12:14):

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 (Dec 07 2022 at 12:17):

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 (Dec 07 2022 at 13:26):

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

Anatole Dedecker (Dec 10 2022 at 16:59):

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 (Dec 10 2022 at 17:09):

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 (Dec 10 2022 at 18:47):

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 (Dec 12 2022 at 14:24):

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 (Dec 16 2022 at 17:44):

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 (Dec 17 2022 at 16:55):

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 (Dec 17 2022 at 21:31):

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 (Dec 17 2022 at 21:36):

Nice!

Anatole Dedecker (Dec 17 2022 at 21:37):

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 (Dec 17 2022 at 21:41):

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 (Dec 18 2022 at 11:05):

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 (Dec 18 2022 at 14:27):

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:

Vincent Beffara (Dec 18 2022 at 14:38):

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 (Dec 18 2022 at 15:12):

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

Anatole Dedecker (Dec 18 2022 at 15:21):

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 (Dec 18 2022 at 16:07):

(deleted)

Kevin Buzzard (Dec 18 2022 at 16:08):

(deleted)

Anatole Dedecker (Dec 18 2022 at 16:27):

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 (Dec 18 2022 at 16:31):

My guess is the second one?

Anatole Dedecker (Dec 18 2022 at 16:32):

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 (Dec 18 2022 at 16:33):

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 (Dec 18 2022 at 16:34):

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 (Dec 18 2022 at 16:34):

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

Yaël Dillies (Dec 18 2022 at 19:05):

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

Anatole Dedecker (Dec 18 2022 at 20:07):

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

Vincent Beffara (Dec 18 2022 at 20:53):

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 (Dec 18 2022 at 21:07):

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 (Dec 18 2022 at 21:08):

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 (Dec 18 2022 at 21:10):

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 (Dec 18 2022 at 21:12):

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 (Dec 18 2022 at 21:13):

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 (Dec 18 2022 at 21:16):

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 (Dec 18 2022 at 21:18):

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 (Dec 18 2022 at 21:27):

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 (Dec 18 2022 at 21:32):

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 (Dec 18 2022 at 22:02):

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 (Dec 18 2022 at 22:06):

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 (Dec 18 2022 at 22:07):

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

Anatole Dedecker (Dec 18 2022 at 22:47):

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 (Dec 18 2022 at 22:55):

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 (Dec 18 2022 at 23:11):

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 (Dec 19 2022 at 08:27):

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 (Dec 19 2022 at 09:20):

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 (Dec 19 2022 at 09:30):

Ah, docs#is_lub.nhds_within_ne_bot

Anatole Dedecker (Dec 19 2022 at 13:22):

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 (Dec 19 2022 at 13:27):

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

Anatole Dedecker (Dec 19 2022 at 13:34):

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 (Dec 19 2022 at 13:36):

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 (Dec 26 2022 at 17:44):

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ä (Dec 26 2022 at 18:51):

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

Anatole Dedecker (Dec 26 2022 at 19:14):

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

Anatole Dedecker (Dec 26 2022 at 23:44):

And here it is: #18017

Anatole Dedecker (Dec 26 2022 at 23:51):

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 (Dec 26 2022 at 23:53):

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)


Last updated: Dec 20 2023 at 11:08 UTC