Distributions & Topological Vector Spaces

Stream: mathlib4

[Michiel Huttener]

1. What is the current state of topological vector spaces and distribution theory in mathlib? Maybe I'm getting confused by the generality, but I could not find any notion of a TVS or a definition of the space of distributions (on some open set) for example.
2. Is anyone working on this? If so, how can I contribute?

[Jireh Loreaux]

Right now we have unbundled topological vector spaces, which you would write like this:

variable {𝕜 V : Type*} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V]
  [TopologicalAddGroup V] [ContinuousSMul 𝕜 V]

(Of course, the NormedField 𝕜 condition could be relaxed.)

[Jireh Loreaux]

I think @Frédéric Dupuis or @Yury G. Kudryashov might be the correct people to ask about the status of this in Mathlib.

[Yury G. Kudryashov]

There are several notions called "distribution". Which one are you talking about?

[Yury G. Kudryashov]

As for TVS, @Jireh Loreaux is right; [Module k V] [ContinuousSMul k V] is the way we write it at the moment.

[Yury G. Kudryashov]

Also, sometimes [Module k V] [ContinuousConstSMul k V] is enough.

[Frédéric Dupuis]

I seem to recall @Anatole Dedecker working on something like this.

[Michiel Huttener]

Distributions in the sense of Schwartz

[Yury G. Kudryashov]

We have docs#SchwartzMap, looking for the dual space.

[Yury G. Kudryashov]

Probably, @Moritz Doll uses continuous linear maps from SchwartzMap instead of introducing a new definition.

[Michiel Huttener]

Thanks for the responses! I'll start by playing around with the type classes. :smile:

[Moritz Doll]

'normal' distributions are the dual of compactly smooth functions, the dual of docs#SchwartzMap is usually called the space of tempered distributions.

[Moritz Doll]

Anatole wrote a lot of stuff for $C_c^\infty$, but I don't know whether it is PR'd

[Moritz Doll]

for tempered distributions you can see from the file that defining things like the dirac delta is not too hard. We are missing a useful criterion to talk about convergence of distributions (the topology is defined, but very abstractly)

[Anatole Dedecker]

I am very busy until tomorrow evening so I won’t comment more right now, but essentially I have quite a lot of plans but not much mathlib-ready code. I worked a bit on it last summer, but I got stuck whilst fighting with docs#ENat (because I wanted to define spaces of order-n distributions for each n in ENat)