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} [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.

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)

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)

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})

@[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)

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

• (_ : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.toSphere μ)) = (_ : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.toSphere μ))

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

• MeasureTheory.Measure.volumeIoiPow n = MeasureTheory.Measure.withDensity (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) fun (r : ↑(Set.Ioi 0)) => ENNReal.ofReal (↑r ^ n)

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))

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.

instance MeasureTheory.Measure.instSigmaFiniteElemRealIoiInstPreorderRealOfNatToOfNat0InstZeroRealInstMeasurableSpaceMemSetInstMembershipSetMeasurableSpaceVolumeIoiPow (n : ℕ) : MeasureTheory.SigmaFinite (MeasureTheory.Measure.volumeIoiPow n)

Equations

• (_ : MeasureTheory.SigmaFinite (MeasureTheory.Measure.volumeIoiPow n)) = (_ : MeasureTheory.SigmaFinite (MeasureTheory.Measure.volumeIoiPow n))

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)

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) [MeasureTheory.Measure.IsAddHaarMeasure μ] (f : ℝ → F) : ∫ (x : E), f ‖x‖ ∂μ = FiniteDimensional.finrank ℝ E • ENNReal.toReal (↑↑μ (Metric.ball 0 1)) • ∫ (y : ℝ) in Set.Ioi 0, y ^ (FiniteDimensional.finrank ℝ E - 1) • f y