Measurable space structure on WithLp

If X is a measurable space, we set the measurable space structure on WithLp p X to be the same as the one on X.

instance WithLp.measurableSpace (p : ENNReal) (X : Type u_1) [MeasurableSpace X] : MeasurableSpace (WithLp p X)

theorem WithLp.measurable_ofLp (p : ENNReal) (X : Type u_1) [MeasurableSpace X] : Measurable ofLp

theorem WithLp.measurable_toLp (p : ENNReal) (X : Type u_1) [MeasurableSpace X] : Measurable (toLp p)

instance WithLp.borelSpace (p : ENNReal) (X : Type u_1) [MeasurableSpace X] (Y : Type u_2) [MeasurableSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [BorelSpace X] [BorelSpace Y] [SecondCountableTopologyEither X Y] : BorelSpace (WithLp p (X × Y))

instance PiLp.borelSpace (p : ENNReal) {ι : Type u_2} {X : ι → Type u_3} [Countable ι] [(i : ι) → MeasurableSpace (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)] : BorelSpace (PiLp p X)

def MeasurableEquiv.toLp (p : ENNReal) (X : Type u_1) [MeasurableSpace X] : X ≃ᵐ WithLp p X

The map from X to WithLp p X as a measurable equivalence.

theorem MeasurableEquiv.coe_toLp (p : ENNReal) (X : Type u_1) [MeasurableSpace X] : ⇑(MeasurableEquiv.toLp p X) = WithLp.toLp p

theorem MeasurableEquiv.coe_toLp_symm (p : ENNReal) (X : Type u_1) [MeasurableSpace X] : ⇑(MeasurableEquiv.toLp p X).symm = WithLp.ofLp

@[simp]

theorem MeasurableEquiv.toLp_apply (p : ENNReal) (X : Type u_1) [MeasurableSpace X] (x : X) : (MeasurableEquiv.toLp p X) x = WithLp.toLp p x

@[simp]

theorem MeasurableEquiv.toLp_symm_apply (p : ENNReal) (X : Type u_1) [MeasurableSpace X] (x : WithLp p X) : (MeasurableEquiv.toLp p X).symm x = x.ofLp