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 = FiniteDimensional.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] [BorelSpace E] (μ : MeasureTheory.Measure E) {s : Set ↑(Metric.sphere 0 1)} (hs : MeasurableSet s) :
    ↑↑(MeasureTheory.Measure.toSphere μ) s = ↑(FiniteDimensional.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] [BorelSpace E] (μ : MeasureTheory.Measure E) :
    ↑↑(MeasureTheory.Measure.toSphere μ) Set.univ = ↑(FiniteDimensional.finrank ℝ E) * ↑↑μ (Metric.ball 0 1 \ {0})
    source
    @[simp]
    theorem MeasureTheory.Measure.toSphere_apply_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] :
    ↑↑(MeasureTheory.Measure.toSphere μ) Set.univ = ↑(FiniteDimensional.finrank ℝ E) * ↑↑μ (Metric.ball 0 1)
    source
    instance MeasureTheory.Measure.instIsFiniteMeasureElemSphereToPseudoMetricSpaceToSeminormedAddCommGroupOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroupOfNatRealToOfNat1InstOneRealInstMeasurableSpaceMemSetInstMembershipSetToSphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] :
    MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.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.FiniteSpanningSetsIn (MeasureTheory.Measure.volumeIoiPow n) (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.instSigmaFiniteElemRealIoiInstPreorderRealOfNatToOfNat0InstZeroRealInstMeasurableSpaceMemSetInstMembershipSetMeasurableSpaceVolumeIoiPow (n : ℕ) :
        MeasureTheory.SigmaFinite (MeasureTheory.Measure.volumeIoiPow n)
        Equations
        • ⋯ = ⋯
        source
        theorem MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] :
        MeasureTheory.MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (MeasureTheory.Measure.comap Subtype.val μ) (MeasureTheory.Measure.prod (MeasureTheory.Measure.toSphere μ) (MeasureTheory.Measure.volumeIoiPow (FiniteDimensional.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 = FiniteDimensional.finrank ℝ E is the dimension of E.

        source
        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) [MeasureTheory.Measure.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