Limit of Lp norm is equal to L∞ norm

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

i.e. $\underset{p\rightarrow\infty}{\lim}\|f\|_{L^p}=\|f\|_{L^\infty}$. Just to double check whether we have this result in Mathlib.

[Etienne Marion]

@loogle Filter.Tendsto, MeasureTheory.eLpNorm

[loogle]

:search: MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm, MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top, and 38 more

[Etienne Marion]

Looks like we don't have it.

[Yongxi Lin (Aaron)]

I am planning to make a PR then