Theorems · Theorem · measure theory
PiLp.volume_preserving_toLp
∀ (ι : Type u_4) [inst : Fintype ι], MeasureTheory.MeasurePreserving (WithLp.toLp 2) MeasureTheory.volume MeasureTheory.volume
The reverse direction of EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, since
MeasurePreserving.symm only works for MeasurableEquivs.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 266 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- ENNRealstatement · cited by 9,879
- Fintypestatement and proof · cited by 7,736
- MeasureTheory.MeasureSpace.volumestatement · cited by 1,323
- WithLpstatement · cited by 345
- MeasureTheory.MeasurePreservingstatement · cited by 259
- MeasurableEquiv.symmproof · cited by 155
- MeasureTheory.MeasurePreserving.symmproof · cited by 43
- MeasurableEquiv.toLpproof · cited by 27
- EuclideanSpace.volume_preserving_symm_measurableEquiv_toLpproof · cited by 4
Cited by5
Results whose statement or proof uses this declaration.
- ZLattice.volume_image_eq_volume_div_covolume'proof · cited by 2
- EuclideanSpace.volume_ballproof · cited by 2
- GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpaceproof · cited by 1
- GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpaceproof · cited by 1
- volume_euclideanSpace_eq_diracproof · cited by 0