English
Given a Haar measure μ on a normed space E, the associated sphere measure μ.toSphere is a measure on the unit sphere S^E with a normalization involving the dimension of E.
Русский
При заданной мере Хаара μ на нормированном пространстве E соответствующая мера μ.toSphere действует на единичной сфере S^E и нормируется размерностью пространства.
LaTeX
$$$\\mathrm{toSphere}(\\mu) = \\dim E \\cdot (\\mu \\circ (\\text{Subtype.val} \\circ (\\text{homeomorphUnitSphereProd}(E))^{-1})|_{\\mathrm{univ} \\times \\dots})$$$
Lean4
/-- If `μ` is an additive Haar measure on a normed space `E`,
then `μ.toSphere` is the measure on the unit sphere in `E`
such that `μ.toSphere s = Module.finrank ℝ E • μ (Set.Ioo (0 : ℝ) 1 • s)`. -/
def toSphere (μ : Measure E) : Measure (sphere (0 : E) 1) :=
dim E •
((μ.comap (Subtype.val ∘ (homeomorphUnitSphereProd E).symm)).restrict (univ ×ˢ Iio ⟨1, mem_Ioi.2 one_pos⟩)).fst
