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)
Equations
@[deprecated WithLp.measurable_ofLp (since := "2024-04-27")]
theorem
WithLp.measurable_equiv
(p : ENNReal)
(X : Type u_1)
[MeasurableSpace X]
:
Measurable ⇑(WithLp.equiv p X)
theorem
WithLp.measurable_toLp
(p : ENNReal)
(X : Type u_1)
[MeasurableSpace X]
:
Measurable (toLp p)
@[deprecated WithLp.measurable_toLp (since := "2024-04-27")]
theorem
WithLp.measurable_equiv_symm
(p : ENNReal)
(X : Type u_1)
[MeasurableSpace X]
:
Measurable ⇑(WithLp.equiv p X).symm
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)
The map from X to WithLp p X as a measurable equivalence.
Equations
- MeasurableEquiv.toLp p X = { toEquiv := (WithLp.equiv p X).symm, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
@[simp]
@[simp]
theorem
MeasurableEquiv.toLp_symm_apply
(p : ENNReal)
(X : Type u_1)
[MeasurableSpace X]
(x : WithLp p X)
: