# Documentation

Mathlib.MeasureTheory.Constructions.HaarToSphere

# Generalized polar coordinate change #

Consider an n-dimensional normed space E and an additive Haar measure μ on E. Then μ.toSphere is the measure on the unit sphere such that μ.toSphere s equals n • μ (Set.Ioo 0 1 • s).

If n ≠ 0, then μ can be represented (up to homeomorphUnitSphereProd) as the product of μ.toSphere and the Lebesgue measure on (0, +∞) taken with density fun r ↦ r ^ n.

One can think about this fact as a version of polar coordinate change formula for a general nontrivial normed space.

def MeasureTheory.Measure.toSphere {E : Type u_1} [] [] (μ : ) :

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 = FiniteDimensional.finrank ℝ E • μ (Set.Ioo (0 : ℝ) 1 • s).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasureTheory.Measure.toSphere_apply_aux {E : Type u_1} [] [] (μ : ) (s : Set ()) (r : ()) :
μ (Subtype.val '' ( ⁻¹' s ×ˢ )) = μ (Set.Ioo 0 r Subtype.val '' s)
theorem MeasureTheory.Measure.toSphere_apply' {E : Type u_1} [] [] [] (μ : ) {s : Set ()} (hs : ) :
= * μ (Set.Ioo 0 1 Subtype.val '' s)
theorem MeasureTheory.Measure.toSphere_apply_univ' {E : Type u_1} [] [] [] (μ : ) :
Set.univ = * μ ( \ {0})
@[simp]
theorem MeasureTheory.Measure.toSphere_apply_univ {E : Type u_1} [] [] [] [] (μ : ) :
Set.univ = * μ ()

The measure on (0, +∞) that has density (· ^ n) with respect to the Lebesgue measure.

Equations
Instances For
theorem MeasureTheory.Measure.volumeIoiPow_apply_Iio (n : ) (x : ()) :
= ENNReal.ofReal (x ^ (n + 1) / (n + 1))

The intervals (0, k + 1) have finite measure MeasureTheory.Measure.volumeIoiPow _ and cover the whole open ray (0, +∞).

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

theorem MeasureTheory.integral_fun_norm_addHaar {E : Type u_1} [] [] [] [] {F : Type u_2} [] [] (μ : ) (f : F) :
∫ (x : E), f xμ = ENNReal.toReal (μ ()) ∫ (y : ) in , y ^ () f y