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.

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} [NormedAddCommGroup E] [NormedSpace E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) (s : Set (Metric.sphere 0 1)) (r : (Set.Ioi 0)) :
    μ (Subtype.val '' ((homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Set.Iio r)) = μ (Set.Ioo 0 r Subtype.val '' s)
    @[simp]

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

    Equations
    Instances For

      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} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] [Nontrivial E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : F) :
        ∫ (x : E), f xμ = FiniteDimensional.finrank E (μ (Metric.ball 0 1)).toReal ∫ (y : ) in Set.Ioi 0, y ^ (FiniteDimensional.finrank E - 1) f y