Theorems · Theorem · measure theory

MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  MeasureTheory.MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (MeasureTheory.Measure.comap Subtype.val μ)
    (μ.toSphere.prod (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ E - 1)))

The homeomorphism homeomorphUnitSphereProd E sends an additive Haar measure μ to the product of μ.toSphere and MeasureTheory.Measure.volumeIoiPow (dim E - 1), where dim E = Module.finrank ℝ E is the dimension of E.

Defined in

Mathlib.MeasureTheory.Constructions.HaarToSphere

Cited by

2 results in Mathlib

Foundations

Depth 275 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasure