English
There is a measure-preserving homeomorphism that decomposes the Haar measure μ on E into the product of its sphere part μ.toSphere and a radial part volumeIoiPow(dim E − 1).
Русский
Существуют мера-лежащие гомеморфизм и разложение меры Хаара μ на E на произведение части сферы μ.toSphere и радиальной части volumeIoiPow(dim E − 1).
LaTeX
$$$\text{MeasurePreserving}(\mathrm{homeomorphUnitSphereProd\,E})(\mu\rvert\uparrow)(\mu^{\mathrm{toSphere}}\times \mathrm{volumeIoiPow}(\dim E - 1)).$$$
Lean4
/-- 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`. -/
theorem measurePreserving_homeomorphUnitSphereProd :
MeasurePreserving (homeomorphUnitSphereProd E) (μ.comap (↑)) (μ.toSphere.prod (volumeIoiPow (dim E - 1))) :=
by
nontriviality E
refine ⟨(homeomorphUnitSphereProd E).measurable, .symm ?_⟩
refine
prod_eq_generateFrom generateFrom_measurableSet
((borel_eq_generateFrom_Iio _).symm.trans BorelSpace.measurable_eq.symm) isPiSystem_measurableSet isPiSystem_Iio
μ.toSphere.toFiniteSpanningSetsIn (finiteSpanningSetsIn_volumeIoiPow_range_Iio _) fun s hs ↦
forall_mem_range.2 fun r ↦ ?_
have : Ioo (0 : ℝ) r = r.1 • Ioo (0 : ℝ) 1 := by simp [LinearOrderedField.smul_Ioo r.2.out]
have hpos : 0 < dim E := Module.finrank_pos
rw [(Homeomorph.measurableEmbedding _).map_apply, toSphere_apply' _ hs, volumeIoiPow_apply_Iio,
comap_subtype_coe_apply (measurableSet_singleton _).compl, toSphere_apply_aux, this, smul_assoc,
μ.addHaar_smul_of_nonneg r.2.out.le, Nat.sub_add_cancel hpos, Nat.cast_pred hpos, sub_add_cancel, mul_right_comm, ←
ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul, mul_div_cancel₀]
exacts [(Nat.cast_pos.2 hpos).ne', Nat.cast_nonneg _]
