Theorems · Definition · measure theory
MeasurableEquiv.toLp
(p : ENNReal) → (X : Type u_1) → [inst : MeasurableSpace X] → X ≃ᵐ WithLp p X
The map from X to WithLp p X as a measurable equivalence.
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- ENNRealstatement and proof · cited by 9,879
- Equivproof · cited by 8,337
- Equiv.symmproof · cited by 3,681
- WithLpstatement and proof · cited by 345
- MeasurableEquivstatement · cited by 269
- WithLp.equivproof · cited by 8
- WithLp.measurable_toLpproof · cited by 8
- WithLp.measurable_ofLpproof · cited by 5
Cited by29
Results whose statement or proof uses this declaration.
- ProbabilityTheory.BrownianReal.projectiveFamilyproof · cited by 19
- MeasurableEquiv.coe_toLpstatement · cited by 8
- PiLp.volume_preserving_toLpproof · cited by 5
- Submodule.measurableEquivProdproof · cited by 5
- EuclideanSpace.volume_preserving_symm_measurableEquiv_toLpstatement and proof · cited by 4
- ProbabilityTheory.IsGaussianProcess.isPreBrownianReal_of_covarianceproof · cited by 4
- WithLp.volume_preserving_symm_measurableEquiv_toLp_prodstatement and proof · cited by 2
- MeasureTheory.charFun_piproof · cited by 2
- MeasureTheory.charFunDual_pi'proof · cited by 1
- ProbabilityTheory.BrownianReal.integral_projectiveFamilyproof · cited by 1
- MeasureTheory.charFunDual_prod'proof · cited by 1