Commit 2025-09-09 18:17 088f81e7

View on Github →

feat: basic properties of toLp and ofLp (#28469) Provide a homeomorph and uniformEquiv version of WithLp.equiv. Show that toLp and ofLp are Lipschitz and anti-Lipschitz, and that toLp is a uniform inducing. Show that evaluation in PiLp is continuous and open.

Estimated changes

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

added theorem PiLp.antilipschitzWith_toLp

added def PiLp.homeomorph

added theorem PiLp.isOpenMap_apply

added theorem PiLp.isUniformInducing_toLp

added theorem PiLp.lipschitzWith_toLp

added theorem PiLp.toEquiv_homeomorph

added theorem PiLp.toEquiv_uniformEquiv

added theorem PiLp.toHomeomorph_uniformEquiv

added def PiLp.uniformEquiv

Modified Mathlib/Analysis/Normed/Lp/ProdLp.lean

added def WithLp.homeomorphProd

added theorem WithLp.isUniformInducing_toLp

added theorem WithLp.prod_antilipschitzWith_toLp

added theorem WithLp.prod_lipschitzWith_toLp

added theorem WithLp.toEquiv_homeomorphProd

added theorem WithLp.toEquiv_uniformEquivProd

added theorem WithLp.toHomeomorph_uniformEquivProd

added def WithLp.uniformEquivProd