Mollification theorem in L^p?

Stream: Is there code for X?

[Olivier Smit]

Proposition234.png Hello everyone, I am curious if this (see attached) theorem or a more general statement has been done in Lean.

[Floris van Doorn]

docs#ContDiffBump.convolution_tendsto_right is very similar, except that $\phi$ is smooth.

[Floris van Doorn]

Oh, it's a bit different, that is pointwise convergence, not convergence in L^p.

[Floris van Doorn]

I don't think we have your precise statement.