HepLean 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.

source
def MeasureTheory.Measure.toSphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) :
MeasureTheory.Measure ↑(Metric.sphere 0 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 = Module.finrank ℝ E • μ (Set.Ioo (0 : ℝ) 1 • s).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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)
    source
    theorem MeasureTheory.Measure.toSphere_apply' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] {s : Set ↑(Metric.sphere 0 1)} (hs : MeasurableSet s) :
    μ.toSphere s = ↑(Module.finrank ℝ E) * μ (Set.Ioo 0 1 • Subtype.val '' s)
    source
    theorem MeasureTheory.Measure.toSphere_apply_univ' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] :
    μ.toSphere Set.univ = ↑(Module.finrank ℝ E) * μ (Metric.ball 0 1 \ {0})
    source
    @[simp]
    theorem MeasureTheory.Measure.toSphere_apply_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] :
    μ.toSphere Set.univ = ↑(Module.finrank ℝ E) * μ (Metric.ball 0 1)
    source
    instance MeasureTheory.Measure.instIsFiniteMeasureElemSphereOfNatRealToSphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] :
    MeasureTheory.IsFiniteMeasure μ.toSphere
    Equations
    • ⋯ = ⋯
    source
    def MeasureTheory.Measure.volumeIoiPow (n : ℕ) :
    MeasureTheory.Measure ↑(Set.Ioi 0)

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

    Equations
    Instances For
      source
      theorem MeasureTheory.Measure.volumeIoiPow_apply_Iio (n : ℕ) (x : ↑(Set.Ioi 0)) :
      (MeasureTheory.Measure.volumeIoiPow n) (Set.Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
      source
      def MeasureTheory.Measure.finiteSpanningSetsIn_volumeIoiPow_range_Iio (n : ℕ) :
      (MeasureTheory.Measure.volumeIoiPow n).FiniteSpanningSetsIn (Set.range Set.Iio)

      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
        source
        instance MeasureTheory.Measure.instSigmaFiniteElemRealIoiOfNatVolumeIoiPow (n : ℕ) :
        MeasureTheory.SigmaFinite (MeasureTheory.Measure.volumeIoiPow n)
        Equations
        • ⋯ = ⋯
        source
        theorem MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] :
        MeasureTheory.MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (MeasureTheory.Measure.comap Subtype.val μ) (μ.toSphere.prod (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ E - 1)))

        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.

        source
        theorem MeasureTheory.integral_fun_norm_addHaar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [Nontrivial E] (μ : MeasureTheory.Measure E) [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure] (f : ℝ → F) :
        ∫ (x : E), f ‖x‖ ∂μ = Module.finrank ℝ E • (μ (Metric.ball 0 1)).toReal • ∫ (y : ℝ) in Set.Ioi 0, y ^ (Module.finrank ℝ E - 1) • f y