Smooth compactly supported functions are dense in L^p

Stream: Is there code for X?

[Moritz Doll]

It seems to me that almost everything is there to prove the statement in the title, but it seems that there is quite a bit of glue missing. Even a smooth version of Urysohn's lemma seems to be missing and the easiest proof I see would go through Geometry.Manifold to use a partition of unity, but that is surely overkill. Does someone have a proof lying around?

[Michael Rothgang]

There are continuous partitions of unity also - would it be easier to prove "smooth compactly supported functions are dense in continuous ... ones" and "continuous compactly supported functions are dense in L^p"?

[Moritz Doll]

Yeah, this is what I first thought, but it seems rather clunky because you end up estimating some norms, which is highly annoying in mathlib, it is already not great on paper. It seems way more elegant to prove smooth Urysohn and repeat the arguments for the continuous version

[Antoine Chambert-Loir]

(deleted)

[Moritz Doll]

Michael Rothgang said:

There are continuous partitions of unity also - would it be easier to prove "smooth compactly supported functions are dense in continuous ... ones" and "continuous compactly supported functions are dense in L^p"?

I actually ended up going that path, because it turned out to be not as bad as I first thought it was. The crucial estimate happened to be in some random file about uniform integrability.

[Michael Rothgang]

Please PR; I also need that statement in the medium term (for Sobolev spaces).

[Moritz Doll]

I definitively will, but probably not in the next couple of weeks. In the meantime, the statements are in mathlib4#29819 in the file Mathlib/Analysis/Distribution/DenseLp.lean (fun fact I just defined abstract Sobolev spaces (as a memSobolev) using the Fourier transform on $\mathbb{R}^n$, but I assume you care more about the manifold case).

[Filippo A. E. Nuccio]

The memSobolevis in the same PR?

[Michael Rothgang]

I also wondered the same thing :-) It's hidden a bit, but it's there: https://github.com/leanprover-community/mathlib4/blob/ab8752f99b4fda64ed8e40fd42bd656479af6901/Mathlib/Analysis/Distribution/FourierMultiplier.lean#L123

[Michael Rothgang]

If f is a complex-valued function defined on a real inner product space and f has temped growth, the PR defines a predicate memSobolev for such functions. In the long run, this could become a lemma "this function is MemLp (in the sense of distributions, not just tempered ones) iff this and that holds".

[Michael Rothgang]

(Side remark: I think the definition should be called MemSobolev, by analogy with MemLp.)

[Moritz Doll]

I guess it is a better name than all of the foo2, foo3 in DenseLp :laughing: (and what happened to foo1?).. the main problematic point at the moment is that the weight (the function g) is usually (1 + |x|^2)^(s/2), but showing that this is of temperate growth is rather tricky unless s = 2.

[Moritz Doll]

The corresponding informal definition is that $f \in H^s(\mathbb{R}^n)$ if and only if $\langle \xi \rangle^s \hat{f} \in L^2(\mathbb{R}^n)$ and using Fourier inversion and Plancherel one can translate that to $\Lambda^s u \in L^2$, where $\Lambda^s = \mathcal{F}^{-1} \langle \xi \rangle^s \mathcal{F}$.

[Yongxi Lin (Aaron)]

Moritz Doll said:

I definitively will, but probably not in the next couple of weeks. In the meantime, the statements are in mathlib4#29819 in the file Mathlib/Analysis/Distribution/DenseLp.lean (fun fact I just defined abstract Sobolev spaces (as a memSobolev) using the Fourier transform on $\mathbb{R}^n$, but I assume you care more about the manifold case).

I checked out this file https://github.com/leanprover-community/mathlib4/blob/cfde5cf76359f0984b0a8d6542dbf273a6abf75e/Mathlib/Analysis/Distribution/DenseLp.lean and it seems like that you are assuming $\mu$ is a Haar measure. I don't think you need some kind of translation invariance for the measure to prove density. In general, $C_c(X)$ is dense in $L^p(\mu)$ for $1\le p<\infty$ if $\mu$ is MeasureTheory.Measure.Regular and $X$ is locally compact Hausdorff. This is at least true for scalar valued functions, and I guess similar results should hold for vector valued functions.

[Moritz Doll]

Thanks for pointing that out. I haven't at all thought about how much the argument generalizes (this is one of the reasons I haven't PR'd it yet). Also @Michael Rothgang please tell me if you do need that result soon, I still have two weeks of other important work, but then I should have time to start PRing this and a lot of other results to mathlib.

[Yongxi Lin (Aaron)]

Moritz Doll said:

Thanks for pointing that out. I haven't at all thought about how much the argument generalizes (this is one of the reasons I haven't PR'd it yet). Also Michael Rothgang please tell me if you do need that result soon, I still have two weeks of other important work, but then I should have time to start PRing this and a lot of other results to mathlib.

Let me know if you need some help. I am happy to make several PR about this because I also need these results for my personal projects.

[Moritz Doll]

#31079 still wip, but we are getting close to a reviewable PR. @Yongxi Lin (Aaron) the reason to use the Haar measure assumption is that the important parts for the bump function use that. You need a uniform bound for how the convolution with a bump changes differs from the function itself in terms of the sup-norm and the necessary ingredients for that are only proved for Haar measures (I haven't thought about whether you can generalize). I don't know whether anyone really cares about smooth approximation for anything but the Lebesgue measure.

[Yongxi Lin (Aaron)]

We do care about smooth approximation in a more general setting! For example if you consider a simple one dimensional ODE of the form $(u(x)/x)'=1$, then naturally you should try to find solutions in $W^{1,p}(\frac{1}{x}dx)$. This kind of singular ODEs/PDEs is why people care about weighted Sobolev space $W^{1,p}(wdx)$, where $w\ge 0$ is a function satisfying the $A_p$ weight condition.

[Yongxi Lin (Aaron)]

We also consider function space like $C([0,T];L^2(\mathbb{R}^n))$ and $L^1([0,T];L^2(\mathbb{R}^n))$ when we consider heat equations or schrodinger equations, so if possible, I think we should also try our best to generalize the density result to certain classes of vector-valued $L^p$ spaces.

[Moritz Doll]

Yeah, everything is vector-valued, but you do need normed spaces. I think the case of density for weighted Lebesgue measures could be adapted rather easily.

[Yongxi Lin (Aaron)]

Oh I see you have already proved the density result for vector-valued functions. That's great!

[Yongxi Lin (Aaron)]

and yes I believe for weighted Lebesgue measures you essentially use the same idea of convolution with a smooth bump function.