Intro: Lukas Miaskiwskyi

Stream: new members

[Lukas Miaskiwskyi]

Hiya, I recently finished my PhD in maths (about Lie theory & Lie algebra cohomology of infinite-dimensional Lie algebras) at the TU Delft in the Netherlands, and am now working in the finance sector -- giving me loads of free time to learn about proof assistants in my free time!

I'm currently only wrapping up the Lean tutorial, but in the long run, I'd love to contribute a little with the things I'm familiar with, perhaps in the direction of functional analysis (Fréchet spaces & topological tensor products?) or Lie theory (perhaps Lie algebra cohomology up to Whitehead's lemma could be a nice goal), though I am also only vaguely aware of how realistic/necessary those are. I'll see how it goes, any recommendations for what to look into are welcome :)

[Anatole Dedecker]

Yay, more functional analysis! We don't have a lot of things in non-normed settings yet (although a few of us are working on it), and setting up a general theory of Fréchet spaces will absolutely be needed at some point.

[Anatole Dedecker]

If you have finished the Lean tutorial and don't feel ready to start contributing yet (although there is no problem in making a messy first PR, reviewers are here to help), I'd say the most natural step would be to have a look at #mil to get a feel for the mathlib way of doing things.

[Lukas Miaskiwskyi]

Thank you for the suggestion :) I will have a look at #mil then! Is there a place or github branch you'd recommend me looking into for the state of functional analysis things? I guess getting familar with the analysis library is a good start, is there some good way to get an overview of what others are working on?

[Moritz Doll]

Hey, we while we don't have a literal definition of a Fréchet space, we have all the properties, so we can state (and hopefully prove) all interesting theorems. A really easy project that you could do to familiarize yourself with the functional analysis stuff is https://github.com/leanprover-community/mathlib/issues/15565
(it might be just one or two lines, but nobody needed it yet)

[Anatole Dedecker]

Yes that would be a nice way to get used to this area of mathlib.

it might be just one or two lines, but nobody needed it yet

Actually, I was a bit optimistic when I told you it would be that easy a few months ago, because we had way less API than I thought. Some of the pieces were added since then, but there are still some API holes to fill. But this is nice for Lukas!

[Anatole Dedecker]

while we don't have a literal definition of a Fréchet space, we have all the properties

Ah yes, I should have mentionned that: we almost surely don't want a frechet_space definition, like we don't have banach_space (we just use docs#normed_space and docs#complete_space). So you should really just prove the interesting theorems for [uniform_space E] [uniform_add_group E] [has_continuous_smul 𝕜 E] [complete_space E] [t0_space E] [(𝓤 E).is_countably_generated]

[Anatole Dedecker]

Note: I think we want to use [t0_space E] [(𝓤 E).is_countably_generated] instead of [metrizable_space E]here because the uniform structure coming from any metric inducing topology wouldn't be defeq to the existing one, whereas the one coming from docs#uniform_space.metrizable_space would be. @Sebastien Gouezel didn't you have a similar problem when working on Polish spaces?

[Sebastien Gouezel]

With polish spaces you just start with a topological space. One should just make sure that, when registering a metric space structure, then the associated topology is defeq to the original one, which is not a problem. In your case, if you assume metrizable_space, would the original uniform structure be automatically propositionally equal to the one coming from a metric, or not?

[Anatole Dedecker]

Sebastien Gouezel said:

In your case, if you assume metrizable_space, would the original uniform structure be automatically propositionally equal to the one coming from a metric, or not?

It would because the additive group is commutative. thanks to docs#uniform_group.to_uniform_space_eq

[Sebastien Gouezel]

This would only work if the metric structure is left-invariant, right? So a strategy using [metrizable_space] would be the following: show that there is a left-invariant metric, then metrize the space using it, with its uniformity adjusted to be defeq to the original one.

[Anatole Dedecker]

Yes I just realized that, there is no reason that a random metric would induce a docs#uniform_group

[Lukas Miaskiwskyi]

Appreciate the discussion & Moritz' suggestion for that small project! Will take me a little bit of time to familiarize myself with the workflow (and to refresh on my FunAna basics), but I'll try to stay on it! Thanks for the warm welcome in any case :)

[Anatole Dedecker]

So really it is not even clear that using metrizable_space here would be mathematically correct, right? Surprisingly, Bourbaki doesn't say wether they mean "metrizable topology" or "metrizable uniform structure" in the definition of Fréchet spaces (and it is interesting to note that they do insist on the distinction between these two in General Topology).
This discussion suggests that I'm not actually sure that I know the right definition of a Fréchet space :upside_down:

[Anatole Dedecker]

Lukas Miaskiwskyi said:

Will take me a little bit of time to familiarize myself with the workflow (and to refresh on my FunAna basics), but I'll try to stay on it!

Take your time, and don't hesitate to ask questions here!

[Anatole Dedecker]

Okay, so to close the "metrizable" discussion, the key fact we'll need is that, for a topological group, metrizability of the topology implies metrizabilty of the uniformity, because one can always get a left-invariant metric inducing the same topology (which Sébastien referred to above). Sorry if I'm just saying trivial things, I never really worked with Fréchet spaces so I'm discovering subtleties.

[Kevin Buzzard]

There is mysterious boundary between the uniform world and the metric world. Maria Ines ran into it when dealing with the difference between valued rings and normed rings. A valuation gives you a uniform structure and a norm gives a metric structure and then you have to make sure that there's no diamond. It sometimes makes me wonder what you real guys see in the metric space structure -- what does it give you that the uniform space doesn't?

[Jireh Loreaux]

There is no notion of Lipschitz maps for uniform spaces right? This is the category where I would expect the primary differences to be.

[Moritz Doll]

Kevin, people in analysis tend to only do so much abstraction as is necessary. If you can get away with only using metric spaces, then that is really nice. Nobody was "oh great let's invent and study general LF-spaces" and later someone found out that $C_c^\infty$ is an LF-space. You would like $C_c^\infty$ to be Fréchet, but very sadly it is not.
If I could I would only use Hilbert spaces, but there are lots of important spaces that are Banach, Fréchet or even LF..

[Moritz Doll]

Anatole Dedecker said:

Note: I think we want to use [t0_space E] [(𝓤 E).is_countably_generated] instead of [metrizable_space E]here because the uniform structure coming from any metric inducing topology wouldn't be defeq to the existing one, whereas the one coming from docs#uniform_space.metrizable_space would be. Sebastien Gouezel didn't you have a similar problem when working on Polish spaces?

I think using [metrizable_space E] is only painful and I don't see any reason to use it. I think it is stated with metrizable because nobody wants to introduce uniformities in textbooks just to say what a Cauchy sequence is

[Kevin Buzzard]

My question about metric spaces in analysis is whether you actually need metrizability or if you can get away with uniformizability.

[Moritz Doll]

in the case we were discussing we already have a uniform structure (since it is a topological group).

[Jireh Loreaux]

Kevin, lots of geometric measure theory works in the category of metric spaces with Lipschitz maps. I think this is something you can't do with just uniformities, but I've been wrong before.

[Kevin Buzzard]

Then I think this is interesting because a lot of what Maria Ines was doing with norms on fields turns out to be perfectly fine if you just restrict to giving the information of the preorder defined by x<=y iff |x|<=|y|.

[Yaël Dillies]

Does this have anything to do with docs#solid?

[Sebastien Gouezel]

A very simple example: from the point of view of uniformities, Lipschitz maps or Hölder maps are just as well behaved (they are uniformly continuous), but from the point of view of analysis Lipschitz maps are much much nicer (for instance, they are differentiable almost everywhere).

[Kevin Buzzard]

My vague idea is that the difference has something to do with the nonarchimedean triangle inequality. The axioms for a norm mention $|x+y|\le|x|+|y|$ so in particular use + on the target object (which is typically nnreal). If you instead beef this up to $|x+y|\le\max\{x,y\}$ then addition is no longer being used on the target which can hence now be any totally ordered group with zero. Conversely, given an inequality coming from a valuation on a field one can reconstruct it up to equivalence from the preorder on the source by letting the target group with zero be the isomorphism classes for the inequality, ie the associated partial order.

[Lukas Miaskiwskyi]

Spent the time since my last message going through #mil and I feel confident enough to try and tackle https://github.com/leanprover-community/mathlib/issues/15565 now! Could I get the necessary branch push permissions? (github username: LukasMias)

A bit anxious about the contributing part since I imagine I'll be writing a bunch of non-ideal and redundant things in the beginning, but I trust that people will be nice to me :D

[Riccardo Brasca]

Invitation sent!

[Riccardo Brasca]

And don't worry about the quality of your code, we've all been there :)

[Patrick Massot]

About that specific issue, you should discuss with @Anatole Dedecker first. But beware he has exams this week so he probably won't answer very soon.

[Moritz Doll]

If you make a PR, feel free to ping me on it and I can have a look.

[Anatole Dedecker]

Congratulations again for your first merged PR!

[Lukas Miaskiwskyi]

Thanks! I'll keep an eye out for more topology stuff to work on independently, but if any of you see some newbie-friendly opportunities I'll always appreciate a ping. This has been very fun so far and I do notice that I'm understanding the flow of things more :) Also: Hope your exams went well Anatole!

[Kevin Buzzard]

Try porting some stuff to Lean 4! We are not yet at topology, but we're moving fast.

[Martin Dvořák]

I think Lukas wanted to do something fun.

[Kevin Buzzard]

Porting is great fun! It's a good way to learn Lean 4, and to learn your way around the maths library. And also when topology is ported it will be even more fun writing it in Lean 4!

[Lukas Miaskiwskyi]

Appreciate the suggestion! So far I had the unfounded impression that was more for the experts who already knew what they were doing, but if that's not a requirement I will keep in mind that it's an option :grinning_face_with_smiling_eyes:

[Mario Carneiro]

Nope, we've opened the floodgates to let anyone work on the port

[Mario Carneiro]

It's hopefully pretty newbie-accessible at this point (although we are improving our processes all the time), and it's probably one of the most impactful things that you can do at this point; usually it's a lot harder to contribute to mathlib so this is a good time if you want to make a contribution

[Kevin Buzzard]

At the beginning porting was hard, because there was less infrastructure, the files were fiddlier, and there was a very limited amount of stuff which could be done. But now we are firmly into basic algebra and there is a bunch of stuff which can be done. Today the rationals became an ordered field.

[Moritz Doll]

Lukas, if you want to help with the port, then you should join the mathlib4 stream and have a look at https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki
The list of portable files is at #port-status and you claim a file by opening a PR for that (PRs work the same way as for mathlib3, you need to get a maintainer to give you non-master push access). Files that don't contain the words 'cast' and 'bits' tend to be more beginner-friendly and also you don't want to have a >500 lines file, that tends to get messy.
One good option would be data.rat.lemmas or even shorter Order.Monotone.Odd (it is only 58 lines).

[Moritz Doll]

Judging from your Lean 3 code, I am very confident that you will learn how to port files very quickly.

[Moritz Doll]

The only annoying thing at the moment is that one has to compile mathlib by hand, there is no leanproject get-c equivalent yet.