Measurable space structure on `WithLp`

Stream: mathlib4

[Etienne Marion]

There has been several discussions about the relations between WithLp and measure theory, for instance #mathlib4 > Diamond with `EuclideanSpace` (`PiLp`) and #mathlib4 > Lacking theorems involving `Measure`, `Prod` and `WithLp`. We are stumbling upon the same thing in the Brownian motion project. There isn't even a measurable space structure on WithLp. In #26249 I simply propose:

import Mathlib.Analysis.Normed.Lp.WithLp
import Mathlib.MeasureTheory.MeasurableSpace.Embedding

open scoped ENNReal

variable {p : ℝ≥0∞}

namespace WithLp

variable {X : Type*} [MeasurableSpace X]

instance measurableSpace : MeasurableSpace (WithLp p X) :=
  MeasurableSpace.map (WithLp.equiv p X).symm inferInstance

end WithLp

Is this too general? I'm guessing that if this has not been done before it's because there are some cases where you want something different (e.g. for p < 1). My question is: are there some cases where we are certain that this is the instance we want, and we can declare it as global, or should instances for WithLp always be local?

[Etienne Marion]

(Not sure if it's related but I am aware of the current refactor of WithLp, and I'm happy to wait until it's done and then modify things accordingly.)

[Etienne Marion]

I have the same question for the topology actually. There is WithLp.instProdTopologicalSpace. Should that also be defined for PiLp? For any WithLp?

[Etienne Marion]

Based on the topological instances for PiLp I deduce that the basic one is just missing. #26261