MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd

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

The theorem `MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd` states that for any additive Haar measure `μ` on a finite-dimensional normed space `E` over the real numbers, the homeomorphism `homeomorphUnitSphereProd E` preserves the measure. In particular, the image of `μ` under this homeomorphism is the product of `μ.toSphere` and `MeasureTheory.Measure.volumeIoiPow (dim E - 1)`, where `dim E = FiniteDimensional.finrank ℝ E` is the dimension of `E`. Hence, this theorem relates the measure on the original space to the measure on the product of the unit sphere and a space of positive real numbers.

More concisely: The homeomorphism of the unit sphere of a finite-dimensional real normed space, under an additive Haar measure, preserves the measure and is equal to the product of the spherical measure and the volume of the open unit ball in the space's complementary subspace.