(Classical) Distributions

Stream: PR reviews

[Anatole Dedecker]

I realized there's no thread here about the stream of PRs about defining (classical, i.e non-tempered) distributions.

As a bit of context, I started work in this direction in the Lean 3 era, and @Luigi Massacci very nicely took care of porting it to current Lean and Mathlib and opening PRs. I am now taking care of these PRs during the review process, and adding some touches on the way.

[Anatole Dedecker]

In the original sequence of PRs by Luigi, the current active one is #30202, which defines the topology on $\mathcal{D}_K^n(E; F)$, where $K$ is a fixed compact set.

[Anatole Dedecker]

To facilitate review, I've also created a parallel stream of PRs for the space $\mathcal{D}^n(\Omega; F)$ of test functions. It starts with #31470, which simply defines the type and some boilerplate API

[Anatole Dedecker]

There is also #31549, which adds some API about docs#tsupport that will be needed later.

[Anatole Dedecker]

@Michael Rothgang has been very nicely reviewing these for now, but I'm sure he'd be glad to have some help, so I'll try to keep this thread up to date!

[Michael Rothgang]

Indeed: I've been reviewing this because I want to build on it (and having it in mathlib simplifies life) --- but I cannot be everywhere at once. Help with reviewing is dearly appreciated!

[Ruben Van de Velde]

I was pretty sure you were everywhere all at once

[Anatole Dedecker]

Next in line is #30236, which shows that the topology on $\mathcal{D}_K^n(E; F)$ is defined by an explicit family of seminorms.

[Anatole Dedecker]

#31533 is now ready for review! It is a boilerplate PR endowing test functions with their algebraic structure, so it should be quite easy to review.

[Anatole Dedecker]

To check that the API created in #30236 is usable, I updated and expanded #30239 (postcomposition by a CLM is a CLM on $\mathcal{D}_K^n$) and #30240 (differentiation is a CLM on $\mathcal{D}_K^n$). I think it works very very well!

[Moritz Doll]

Nice proof of fderivCLM. This is exactly what I would hope it to be :smile:

[Anatole Dedecker]

Anticipating a bit, in the other sequence of PRs, I've just finished polishing #31806 which defines the topology on the whole space of test functions and proves its universal property. It only depends on the easy #31533, if this motivates anyone!

[Anatole Dedecker]

#31806 (topology on test functions) is now ready for review!

[Michael Rothgang]

I presume #30239 is another PR ready for review?

[Anatole Dedecker]

Yes! This one is about postcomposition by a CLM, which gives a CLM on test functions supported in a fixed compact set.

[Anatole Dedecker]

I just opened #32210, which bundles iteratedFDeriv as a bare linear map on test functions (no prerequisites).

Continuity will have to wait, in the iterated case, for a version of docs#norm_iteratedFDeriv_fderiv about iterated derivative of an iterated derivative, but even without this I'll be able to use it to prove that the map $\mathcal{D}^n_K(E, F) \to \mathcal{D}^n(\Omega, F)$ is actually a topological embedding.

[Anatole Dedecker]

#32219 (easy): $\mathcal{D}^n_K(E, F)$ is T3

[Anatole Dedecker]

#32222 (+28) is also quite elementary. It gives another characterization of the topology on $\mathcal{D}^n_K$ in terms of IsEmbedding. This is useful because we have a lot of API about IsEmbedding, which avoids having to rewrite/compare the topologies by hand.

[Anatole Dedecker]

#32233: instantiate docs#ContinuousEval for docs#BoundedContinuousFunction

[Michael Rothgang]

#32228 (+65 lines): coercion to bounded continuous functions as a CLM on TestFunction

[Anatole Dedecker]

#32353 defines the TVS of vector-valued distributions on an open set of a finite dimensional normed space! It has essentally no Lean content, but it contains an extensive module docstring detailing various design choices, along with mathematical references.

[Anatole Dedecker]

I would completely understand if you prefer to wait to see a more developped theory before moving forward, but reviews on the docstring are welcome already.

[Anatole Dedecker]

(I got a bit scared when checking references: it turns out that, for spaces of distributions of order at most n, the correct topology is compact convergence, not bounded convergence, which I had not realized. This is not a problem for $\mathcal{D}'$ itself, since $\mathcal{D}$ is a Montel space)

[Anatole Dedecker]

#32368 (+33): tsupport version of some support lemmas

[Anatole Dedecker]

#32390 (easy): we have →SL_c notation for docs#CompactConvergenceCLM, but not the →L_c variant. This PR fixes that.

[Anatole Dedecker]

#32395 (+33/-5): specialize docs#ContinuousLinearMap.precomp_uniformConvergenceCLM and docs#ContinuousLinearMap.postcomp_uniformConvergenceCLM to the topology of compact convergence

[Anatole Dedecker]

And thanks everyone for the reviews!!!

[Anatole Dedecker]

#32401: the natural continuous linear map $\mathcal{D}^{n_1}(\Omega_1) \to \mathcal{D}^{n_2}(\Omega_2)$ when $n_2 \leq n_1$ and $\Omega_1\subseteq\Omega_2$

I'm not sure wether I should split these into "the monotonicity in n" and "the monotonicity in $\Omega$".

[Anatole Dedecker]

I've just created https://github.com/orgs/leanprover-community/projects/30 to track distribution PRs. @Moritz Doll I should have given you the rights to edit the project by adding your own PRs (I can also create a separate project if you prefer)

[Laura Monk]

Hi! Sending a message on the correct chat this time. Thanks for the advances, I will try and look at the files this afternoon :)

[Anatole Dedecker]

Thanks a lot! Unfortunately I have been busy with other things this week (namely, working on my PhD :sweat_smile:) so there's not that many PRs ready for review right now :/ I will update some of them so that there are things to review, but I can't spend a lot of time on this today...

[Anatole Dedecker]

Do you need something specific that I could prioritize?

[Anatole Dedecker]

#32330 (+38, -0): postcomposition by a CLM as a CLM on test functions

[Anatole Dedecker]

#30240: differentiation as a continuous linear map on $\mathcal{D}^n_K$

[Anatole Dedecker]

This last one highlights that, with the current setup, the most convenient way to define an operation on test functions involves quite a bit of boilerplate (e.g one has to define the linear map on $\mathcal{D}^n_K$, then its continuous version, then the linear map on $\mathcal{D}^n$, and then the continuous version of that).

Unfortunately I don't have a very good solution for now. I think/hope that TestFunction.mkCLM will be easy enough to use when concretely defining definitions, but for more complicated use cases it's a bit too painful to do everything at the same time.

[Anatole Dedecker]

I am definitely taking suggestions here, but I also prefer an approach with some boilerplate but easy proofs than an approach with less boilerplate but painful proofs.

[Laura Monk]

Oh I meant I would have a look at what is already there, don't worry!
I think I will need the notion of support of a distribution notably.

[Laura Monk]

In the long run I need Lemma 4.7 from this article.

[Anatole Dedecker]

This is helpful, it means I need to start doing for $\mathcal{E}$ the analog of what I am doing for $\mathcal{D}$ so that we get compactly supported supported distributions $\mathcal{E}'$

[Laura Monk]

Are you interested in doing so? It would be super helpful, obviously I would help with the reviewing.

[Anatole Dedecker]

I am, I just cannot guarantee that I'll do it very fast. But $\mathcal{E}$ is conceptually simpler than $\mathcal{D}$ (as there are no inductive limits) so it should be relatively easy.

[Laura Monk]

Amazing! And there is no rush at all :)