Distribution theory

Stream: maths

[Anatole Dedecker]

Hello everyone ! I'm planning to work with @Patrick Massot on teaching distribution theory to Lean during this semester. Did anyone have plans about it ? (cc @Heather Macbeth @Yury G. Kudryashov @Kalle Kytölä @Rémy Degenne @Sebastien Gouezel)

Also, do you know if it has ever been formalized in any other proof assistant ?

[Moritz Doll]

I also want to do this, I was mainly thinking of implementing tempered distributions. I am still working on the topology for locally convex spaces (aka family of seminorms give topological vector space).

[Kevin Buzzard]

There's an important theory of Frechet spaces over p-adic fields, I hope such generalities aren't forgotten when we get around to this :-) @Jeremy Teitelbaum might have something to say about this sort of thing

[Kalle Kytölä]

Sounds fantastic! I did not have any plans about distribution theory, but I will be super happy if and when that makes it to mathlib.

(Until March likely my only Lean will be walking through a few easy metric topology proofs with the students of an undergraduate course. I believe in Lean's infoview for the "exploring proofs" purpose, but let's see if the students agree...)

[Yury G. Kudryashov]

I'm sorry for a stupid question: do you mean https://en.wikipedia.org/wiki/Distribution_(mathematics) or https://en.wikipedia.org/wiki/Distribution_(differential_geometry) ?

[Anatole Dedecker]

First one

[Patrick Massot]

@Moritz Doll What do you intend to formalize exactly, and when? We don't want to duplicate too much effort.

[Yaël Dillies]

How are locally convex spaces going btw?

[Yaël Dillies]

I'm happy to help/take over whenever.

[Moritz Doll]

@Patrick Massot I haven't made a real plan yet, but I wanted to define the Schwartz space and show that the Fourier transform is well-defined there.

[Moritz Doll]

@Yaël Dillies there is this https://github.com/leanprover-community/mathlib/pull/11329 and I have some code for defining the module_filter_basis, but in the later there are lots of sorry's.

[Jeremy Teitelbaum]

Schneider's Nonarchimedian Functional Analysis tells the whole story. Over p-adic fields the theorems are mostly the same but the approach is different. It's easier in some ways, since convergence is easier; but you sometimes need to work over non-locally compact fields, which complicates life in other ways.

[Yao Liu]

Newbie to Lean, I'd like to contribute, but first learn by watching how others do it. Didn't know about p-adic distributions.

Schwartz space S' is over R^n, while D' and E' can be over any open subset of R^n. Are there needs for distributions over other manifolds?

[Filippo A. E. Nuccio]

In the future I would be very happy to contribute to the Nonarchimedean part of the story, but I certainly can't engage myself now. I will try to follow and to join the project at a certain point if there will still be things to do.

[Gunnar Þór Magnússon]

Are there needs for distributions over other manifolds?

It may be out of scope for mathlib, but people use distributions on manifolds to prove advanced things in Kahler geometry, for example.

[Johan Commelin]

I don't think that should be out of scope. Sure, we can't do that now. But we shouldn't paint ourselves in a corner. It's good to look far ahead (-;

[Notification Bot]

This topic was moved by Johan Commelin to #general > scope of mathlib

[Moritz Doll]

@Yaël Dillies the add_group_topology and has_continuous_smul is now sorry-free, but I am still missing the statements and proofs that in that case of a single seminorm the topology coincides with the semi_normed_space-topology and continuity of linear maps in terms of seminorms.

[Moritz Doll]

#11604 :tada: still quite rough (the names are not really good, missing documentation), but results are there.

[Anatole Dedecker]

@Moritz Doll @Yaël Dillies I'm the one to blame because I've been doing things on my own without keeping myself up to date with what was being done, but we should try to coordinate on this. FYI I'm doing this as a school project, so I'm doing things in a separate repo to keep track of everything, but the goal is definitely to teach this to mathlib.

I started working on defining distributions, which mostly means defining the topology on $C_c^\infty(U)$, and since I didn't want to develop the theory about seminorms I went the "convex neighborhood basis" to define locally convex spaces. After a bit of thinking (I've just discovered this part of maths), this is what I'm planning to do in the next few days :

• define the topology on $C^\infty(U)$ as the initial topology generated by the iterated differentials $D^n : C^\infty(U) \to C_0(\text{continuous }n\text{-linear maps on }E)$, and I can easily prove this is a LCTVS by proving that being a LCTVS is preserved by taking the Inf of topologies or pulling them back along linear maps. Note I didn't used any seminorms, because I think the purely topological way is easier since mathlib already has the compact open topology on $C^0$, and I think this would give better definitional properties because we don't have to choose one family of seminorms among all the ones that give the same topology
• then define the topology on $C_K^\infty(U)$ by pulling back along the inclusion in $C^\infty(U)$ (again, still a LCTVS)
• then, defining the topology on $C_c^\infty(U)$. Since the usual pushforward and Sup of topologies do not preserve LCTVS, I thought the simplest way to do it would be to take the Inf of all LCTVS topologies which make all the inclusions from $C_K^\infty(U)$ continuous, which we know gives an LCTVS, which gives us the inductive limit almost for free.

If you are already close to having a definition using seminorms, it works for me, and I can start using it as soon as we know that it's preserved by Inf and pullback along a linear map. That said, I think we should keep in mind that there are often a lot of choices when defining a topology using seminorms, so maybe we should have an class locally_convex_space with the neighborhood definition and a separate generated_by_seminorms predicate that makes the family of norms explicit ?

Moritz, I saw you started working on defining the Schwartz space. How soon do you want to start working on tempered distributions ? I don't have a clear idea about how to relate distributions and tempered distributions in lean yet (as a subset vs as a distinct construction with continuous inclusion), but how do you want to split the work ? I could focus on general distributions and you could work on tempered distributions and Fourier transform for example, would that be ok to you ?

[Yaël Dillies]

Anatole Dedecker said:

That said, I think we should keep in mind that there are often a lot of choices when defining a topology using seminorms, so maybe we should have an class locally_convex_space with the neighborhood definition and a separate generated_by_seminorms predicate that makes the family of norms explicit ?

Can't agree more. That's exactly what I was referring to in https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311604.20Topology.20induced.20by.20seminorms. We want to be able to state that a space is locally convex without needing it to be defined from seminorms. And Moritz's current approach seems to not have that.

[Yaël Dillies]

What we want to be able to do is to generate a topology from a family of seminorms, but that's unrelated to stating that a topology is locally convex.

[Yaël Dillies]

But yeah also Anatole it would've been nice to keep us updated on that :confused: It's not duplicating any of my work, so I'm not fussed, but I don't know about Moritz.

[Anatole Dedecker]

Yaël Dillies said:

What we want to be able to do is to generate a topology from a family of seminorms, but that's unrelated to stating that a topology is locally convex.

Well that's not unrelated since we could put data in the class like it's done for e.g metric spaces, but the the thing is we don't want to do that here since the data is highly not canonical.

[Yaël Dillies]

Yes, precisely.

[Yaël Dillies]

Sorry if I haven't been putting my thought into words enough :sweat_smile:

[Yaël Dillies]

Unless someone knows of a useful canonical representation of a locally convex space by a family of seminorms, I'm all for hiding the family away in an existential, or using the convex basis approach which I like too.

[Anatole Dedecker]

Yaël Dillies said:

But yeah also Anatole it would've been nice to keep us updated on that :confused: It's not duplicating any of my work, so I'm not fussed, but I don't know about Moritz.

Of course I understand and I'm sorry for that. Note that I don't actually have a lot of code yet, these are mostly plans I made for starting working on this, which is why I'm absolutely fine with adapting what I have to what has been done. Moritz, please tell me if my plans are overlapping yours in any way, I'll be happy to adapt !

[Patrick Massot]

Yaël, that very thread you're reading starts with Anatole telling us he would like to start working on this.

[Patrick Massot]

And then Moritz telling us about his intentions. I thought it was ok that Moritz would focus on tempered distributions and Anatole on general ones.

[Yaël Dillies]

I think you're missing all the previous threads about locally convex spaces, Patrick :grinning:
But I agree there shouldn't be a tremendous overlap.

[Anatole Dedecker]

In fact, I initially thought I could just not mention local convexity until I needed it, so I could just wait that you or Moritz defined it. But then I realized I really needed it for the definition so I made a quick version of it, but really that should be easily replaceable by what ends up into mathlib.

[Moritz Doll]

Yaël Dillies said:

Anatole Dedecker said:

That said, I think we should keep in mind that there are often a lot of choices when defining a topology using seminorms, so maybe we should have an class locally_convex_space with the neighborhood definition and a separate generated_by_seminorms predicate that makes the family of norms explicit ?

Can't agree more. That's exactly what I was referring to in https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311604.20Topology.20induced.20by.20seminorms. We want to be able to state that a space is locally convex without needing it to be defined from seminorms. And Moritz's current approach seems to not have that.

Defining locally convex is completely independent from what I did in the PR. As soon as you have a definition for that it should be straightforward to prove that with_seminorms p has is_locally_convex.

[Moritz Doll]

As for tempered distributions vs distributions: I would think that the definitions are completely separate and that there is a coe from tempered distributions to distributions. I am not too afraid that the work actually overlaps, we have to be careful when defining stuff that is useful for both tempered and normal distributions.

[Moritz Doll]

but maybe it might be a good idea to organize the stuff we want to do (or just want to have and not working yet) somehow. I've seen that there these github projects, are they any good?

[Moritz Doll]

Just to let everyone (@Yaël Dillies @Anatole Dedecker ) know what I am planning on doing. I need some abstract nonsense results to be able to prove continuity results efficiently. In particular, that continuity implies local boundedness and if the space is pseudometrizable (probably I will use something equivalent), then the converse is also true. This will also remove some ad-hoc lemmas in locally_convex/with_seminorms.

[Moritz Doll]

As for the interaction between tempered distributions and distributions: we should prove that $C_c^\infty \subset \mathcal{S}$ and then prove an abstract result that this implies that $\mathcal{S}' \subset \mathcal{D}'$ (maybe it already exists, I haven't looked). I am pretty certain that inclusions should become continuous injections in Lean.

[Anatole Dedecker]

I will answer some precise points later, but I guess you will need the topology on continuous linear maps between two TVS rather quickly then ? Which means I should get back to work on the few PRs leading to this and make the final one two. Sorry I put that aside when working on Hilbert spaces.

[Moritz Doll]

Don't worry, there is way too much to do in analysis and having compact and positive operators is amazing.

[Anatole Dedecker]

Moritz Doll said:

we should prove that $C_c^\infty \subset \mathcal{S}$ and then prove an abstract result that this implies that $\mathcal{S}' \subset \mathcal{D}'$ (maybe it already exists, I haven't looked).

The abstract result is just the fact that the precomposition of continuous linear maps by a fixed continuous linear map is a continuous linear map, right? If so, this is one of the results I was planning to do in the PR for strong topology so this won't be a problem

[Anatole Dedecker]

Oh but we probably want it to be a docs#embedding, so I need to plan for this

[Anatole Dedecker]

Moritz Doll said:

In particular, that continuity implies local boundedness and if the space is pseudometrizable (probably I will use something equivalent), then the converse is also true

The easy direction is docs#is_vonN_bounded.image

[Anatole Dedecker]

For the other direction, I haven't thought about it in a while, but the right notion here is bornological spaces right ?

[Moritz Doll]

For pseudometrizable spaces one can prove it directly, but in general you need bornological spaces. In particular, for LF I think it is best to do the whole abstract theory.

[Moritz Doll]

i.e., for Schwartz its relatively easy, but for $C_c^\infty$ it will be really tedious

[Moritz Doll]

I don't think I will have the time to do the bornological space story (at least not this year).

[Anatole Dedecker]

Oh yeah of course, I didn’t mean that you had to do it, I was just wondering about we will ultimately want

[Yaël Dillies]

Sorry, I don't think I will be of much help here

[Moritz Doll]

Moritz Doll said:

For pseudometrizable spaces one can prove it directly, but in general you need bornological spaces. In particular, for LF I think it is best to do the whole abstract theory.

I've tried doing that, but I already failed at finding the correct formulation. docs#is_vonN_bounded.image uses in a sense unbundled locally bounded maps, but there are also a bundled variant in docs#locally_bounded_map but if one uses that then I don't see avoid any loops for the instance search. So maybe what docs#is_vonN_bounded.image did is the way to go? @Jireh Loreaux you might have told me what the solution would be for that at ICERM, but I don't remember.

[Jireh Loreaux]

I don't know if I have the solution, and there may be bad effects that I'm missing, but I thought a possible solution was just to have bornological spaces as a Prop mixin that says given a TVS with a bornology, its bornology is propositionally equal to the docs#bornology.vonN_bornology. Is there a reason this is a bad idea? (Note: I haven't checked the definition of bornological space recently, but I think that's what it means.)

[Yaël Dillies]

No, this is a good idea. That's what's done for docs#discrete_topology, for example.

[Jireh Loreaux]

Wait, maybe this isn't what it means.

[Yaël Dillies]

Yeah I don't think that's what a bornological space is

[Anatole Dedecker]

Yes but there is no more data than topology and bornology so this approach should work

[Anatole Dedecker]

Does it really solve Moritz’s problem though ?

[Jireh Loreaux]

Fixing what I said above: the right way to do (quasi-)bornological space in mathlib is just to define bornivore and then the class is the mixin which says ∀ s : set X, bornivore s → s ∈ 𝓝 0.

But apparently this isn't the problem, which means I misunderstood something above. @Moritz Doll , can you specify what instance loop problems you mean? (also, looping problems should be solved with Lean 4 type class search, so this is only a temporary problem.)

[Moritz Doll]

if you have a typeclass locally_bounded and a typeclass continuous_linear_map, then you cannot make both directions of the equivalence instances. The question was how to deal with it. The person that wrote docs#is_vonN_bounded.image ignored the fact that we have locally_bounded and it seems that at the moment this might be the smartest decision

[Jireh Loreaux]

Yeah, for this I think the solution is to wait for Lean 4.

[Anatole Dedecker]

The reason I did not use docs#locally_bounded_class in docs#is_vonN_bounded.image is that I’m still not happy with the fact that we have use typeclasses for bornologies, and that would make this awkward to state

[Anatole Dedecker]

(I mean I’m happy with having a has_canonical_bornology typeclass but bornologies should not be used as typeclasses by default imo, but that’s another subject)

[Anatole Dedecker]

Oh but we probably want it to be a docs#embedding, so I need to plan for this

I thought about this again while writing documentation for #14534 (this is the base PR for strong topology) and I've done enough API for the uniform_inducing part to be easy :happy: so I'll add it (EDIT: it's the wrong side of composition :face_palm: ). The injectivity should be easy if we know that test functions are dense in the Schwartz space (I think that is true?)

[Anatole Dedecker]

I'll have a deeper look tomorrow

[Moritz Doll]

yes, this is true and I can prove it once the Schwartz PR is merged (or I am finished with the first part of the bilinear form refactor, whatever happens first)

[Anatole Dedecker]

Before I try too hard to think about it, do you know if it actually is a docs#embedding ? Everyone online seems to be happy with "we have a continuous linear injection so let's say it's a subset" but it feels wrong to say that if it's not an embedding. I'm going to look into Schwartz's book if I see something about it.

[Moritz Doll]

hm, I am not sure to be honest, because I don't know how to translate the inducing condition into a seminorm condition. For any fixed $C_c^\infty$ function and every seminorm that induces the $C_c^\infty$-topology you find a Schwartz seminorm that can be estimated above and below by some positive constants (only depending on the domain, because you have get rid of the weighting factor in the Schwartz seminorm and that depends on the domain of the $$C_c^\infty$ function). If that is proves inducing, then we have an embedding, but if the estimate has to be uniformly for all $C_c^\infty$ functions, then I guess that we are out of luck

[Moritz Doll]

anyways all that is ever needed is continuous and injectivity and that we have for sure

[Anatole Dedecker]

The inclusion $\mathcal{D} \subseteq \mathcal{S}$ can't be an embedding, because there is no reason that a sequence of $C_c^\infty$ functions converging to 0 in the Schwartz space would have their support eventually contained in a fixed compact (and https://math.stackexchange.com/questions/1735079/do-tempered-distributions-form-a-topological-subspace-of-the-space-of-distributi indeed gives a counter example)

[Anatole Dedecker]

But there is still the question of the inclusion of the strong duals $\mathcal{S'} \subseteq \mathcal{D'}$

[Anatole Dedecker]

It looks like this isn't true either: https://math.stackexchange.com/questions/3905508/convergence-in-distribution-space-and-tempered-distribution-space

[Moritz Doll]

Maybe more a reminder for myself: we probably don't need a definition of Fréchet spaces (maybe later when we have bornological spaces), it should just be uniform_add_group + complete_space + first_countable_topology (or countable_uniformity) + locally_convex + regular. In particular, we have no choices of seminorms in that definition and we don't need metrizable.
To get an equivalence to the usual definition there is the part missing that you find countable family of seminorms if the space is first countable, but this should be easy (and I will not do it, since it is never needed in practice).

[Moritz Doll]

@Anatole Dedecker did you wrote any code for $C^k(X)$ as a locally convex space? Since we define the Dirac delta via the injection to bounded_continuous_function it seems to be very reasonable to do the same thing with fderiv but using $C^1$ instead.

[Moritz Doll]

Moreover, there is the question whether we want to have lots of funny classes for all of these function spaces (probably yes), but then it might be annoying to define these since we probably want to bake things like Sobolev embedding theorems into them..

[Anatole Dedecker]

Moritz Doll said:

Anatole Dedecker did you wrote any code for $C^k(X)$ as a locally convex space?

I assume you mean "$C^k$ with all derivatives bounded"? If so indeed I have some code about it. I was actually planning to skip it and go directly to support conditions instead of boundedness when PR-ing to mathlib, but now I realize than you need the bounded case for the Schwartz space

it seems to be very reasonable to do the same thing with fderiv but using $C^1$ instead

Indeed I did something along these lines to define fderiv as a continuous linear map from test functions to test functions, but I think it is a bit more tricky than just embedding into $C^1$ because you also want Schwartz space as the codomain, does that sound right?

[Anatole Dedecker]

Moritz Doll said:

Moreover, there is the question whether we want to have lots of funny classes for all of these function spaces (probably yes)

Indeed, part of the reason while I've not taken the time to PR anything about test functions yet is that it feels bad to introduce and develop API for spaces which are essentially useless for anything else than defining test functions and their topology x)

[Moritz Doll]

If you are not convinced that we need the classes right now, we should probably skip them for now and if we see that they are useful we can still refactor.

[Moritz Doll]

@fderiv: I have finished #16756 and I might have to retract my claim that going through $C^k$ helps for that.

[Moritz Doll]

I've found a very minor naming inconsistency: in the measure theory parts the Dirac delta distribution is called measure_theory.measure.dirac and I called it schwartz_map.delta, should I rename it to schwartz_map.dirac?

[Kevin Buzzard]

I guess delta has other meanings both in math and CS whereas Dirac is less ambiguous