English
A refinement of the prior toSphere identity giving an exact expression for μ.toSphere on measurable sets via a transformed image under a homeomorphism.
Русский
Уточнение тождества toSphere, дающее точное выражение для μ.toSphere на измеримых множествах через преобразование изображения гомоморфизмом.
LaTeX
$$$\\mu.toSphere(S) = \\dim E \\cdot \\mu(\\text{transformed region})$$$
Lean4
theorem toSphere_apply' {s : Set (sphere (0 : E) 1)} (hs : MeasurableSet s) :
μ.toSphere s = dim E * μ (Ioo (0 : ℝ) 1 • ((↑) '' s)) := by
rw [toSphere, smul_apply, fst_apply hs, restrict_apply (measurable_fst hs),
((MeasurableEmbedding.subtype_coe (measurableSet_singleton _).compl).comp
(Homeomorph.measurableEmbedding _)).comap_apply,
image_comp, Homeomorph.image_symm, univ_prod, ← Set.prod_eq, nsmul_eq_mul, toSphere_apply_aux]
