Frequency-side Sobolev definitions

Stream: mathlib4

[Michael Mlynarczyk]

Hello everyone,

I work on turbulence analysis (JHTDB) and would like to formalize some of the Fourier-side Sobolev machinery.

Mathlib has spatial Sobolev theory, but the frequency-side definitions seem to be missing, so I was hoping to open a small PR that adds just the basic, reusable definitions.

My proposed file:
Analysis/Sobolev/Fourier.lean

Content:
The Bessel potential multiplier

hsMul s ξ := (1 + ‖ξ‖^2)^(s/2)

The frequency-side (H^s) norm squared on inner product spaces (via Plancherel).

My question is: would Analysis/Sobolev/ be the preferred directory for this, or should it live under Analysis/Fourier/ instead?

I didn’t see any conflicting PRs, but please let me know if I missed something.

Thanks!

[Moritz Doll]

I didn't open an PR for that, but I have all of the code.

[Yongxi Lin (Aaron)]

@Moritz Doll Have you considered defining the more general Sobolev–Slobodeckij space or even Besov spaces? Sobolev spaces are really speciall cases of these spaces and since Mathlib aims at generality, I wonder whether we should define these spaces first.

[Moritz Doll]

Yeah, but doing that will take way more effort and I think we want to have both definitions anyway. Definitively Besov spaces are on my list, but not in the near future. Also the same is true for the $W{k, p}$ spaces, where you end up with Triebel Lizorkin spaces. I haven't checked but I am sure we are missing quite a bit to do either of those

[Michael Mlynarczyk]

@Moritz Doll Excellent, thanks for the update.
If you have a branch that is close to ready, would you be willing to open a PR? I'd be happy to assist with the review if needed.

@Yongxi Lin (Aaron) Totally agree Besov/Triebel-Lizorkin is the end goal. I also feel the concrete $L^2$-based $H^s$ definition will be essential for those of us doing classical PDE analysis!

Thanks again.

[Moritz Doll]

Also the whole thing is more complicated: if you want negative order Sobolev spaces, then you need to talk about (classical/tempered) distributions, in the case of $H^s$ that would be tempered distributions. Even without that it is more convenient to define $H^s$ as a subspace of $\mathcal{S}'$ rather than a subspace of $L^2$, because dealing with functions only being defined almost everywhere is somewhat annoying.

[Moritz Doll]

#29948, #32297, #31757 all are reviewable and used for the definition of Sobolev spaces. #29819 contains a toy-model (I haven't updated it to reflect that I have everything that is needed for the real thing, because I think that anyone would care)

[Filippo A. E. Nuccio]

With @Floris van Doorn and @Michael Rothgang we've been working towards the definition and first properties of Sobolev spaces, resulting in #32305. On the final lines we list what we're heading to, beyon the boilerplate constructions that are already in place. The main points are

1. Banach property
2. Monotonicity in the exponent
3. Reflexivity
4. Sobolev embedding theorem.

For all this, we're basically following Adam's classical book, but in a mathlib-adapted way.

[Yongxi Lin (Aaron)]

Is there any chance that this project will have open issues like the ones in the Brownian Motion project? I am happy to help accelerate the process of constructing the Sobolev space theory in Mathlib.

[Michael Rothgang]

My understanding is that Sobolev spaces for non-integer or negative exponents require the integer case anyway, so that's a useful start in any case

[Michael Rothgang]

Yongxi Lin (Aaron) said:

Is there any chance that this project will have open issues like the ones in the Brownian Motion project? I am happy to help accelerate the process of constructing the Sobolev space theory in Mathlib.

Thanks for asking! We had originally not planned our project this way, but we'll discuss whether this makes sense for us.

[Sébastien Gouëzel]

Michael Rothgang said:

My understanding is that Sobolev spaces for non-integer or negative exponents require the integer case anyway, so that's a useful start in any case

I'm not sure about that. Isn't the standard Fourier-theoretic definition just about the integrability of some function built out of the Fourier transform?

In any case, we will need the elementary definition for integer values of the parameters, because it's sometimes the most convenient to use. But for the properties like monotonicity, Sobolev embeddings, completeness and so on, I think it would make sense to do them directly in the general case, and then derive the properties for integer smoothness from them.

[Moritz Doll]

That is $H^s$ (which is what I am doing), Michael and Filippo are doing $W^{k,p}$. When $p = 2$, they do agree, but the Fourier multiplier definition does not give the same thing for $p \not = 2$.
However, I think for non-integer order you can still define the $W^{k,p}$-Sobolev space directly (I haven't checked, but probably some Hölder-like norm should do), for negative order I am not aware of how to define it directly. Maybe if you do the predicate first and the bundled version only once you can define everything, you will not get into a mess with multiple definitions.

[Sébastien Gouëzel]

I was thinking of $H^{s,p}$, i.e., those distributions such that $\mathcal{F}^{-1}((1+|\xi|^2)^{s/2} \mathcal{F}f)$ belongs to $L^p$. They coincide with $W^{k,p}$ for integer $k$ if I'm not mistaken, but they form a whole scale indexed by real exponents.

[Sébastien Gouëzel]

But looking at Wikipedia I see there is also a scale $W^{s,p}$ which indeed has a different definition for integer and non-integer $s$, and for which the definition for non-integer $s$ is essentially based on the one for integer $s$.

[Michael Rothgang]

Sébastien Gouëzel said:

But looking at Wikipedia I see there is also a scale $W^{s,p}$ which indeed has a different definition for integer and non-integer $s$, and for which the definition for non-integer $s$ is essentially based on the one for integer $s$.

That's the one I meant.

[Floris van Doorn]

Adam's book discusses them both: using complex interpolation from the integer spaces in 7.57, and the characterization in terms of the Fourier transform in 7.62-7.63 (up to equivalence of norms).
The direct definition makes it interesting to do the general case first.