Integrals in Space

i. Overview

In this module we give general properties of integrals over Space d. We focus here on the volume measure, which is the usual measure on Space d, i.e. dx dy dz.

ii. Key results

• volume_eq_addHaar : The volume measure on Space d is the same as the Haar measure associated with the basis of Space d.
• integral_volume_eq_spherical : The integral of a function over Space d.succ with respect to the volume measure can be expressed as an integral over the unit sphere and the positive reals.
• lintegral_volume_eq_spherical : The lower Lebesgue integral of a function over Space d.succ with respect to the volume measure can be expressed as a lower Lebesgue integral over the unit sphere and the positive reals.

A. Properties of the volume measure

theorem Space.volume_eq_addHaar {d : ℕ} : MeasureTheory.volume = basis.toBasis.addHaar

theorem Space.volume_closedBall_ne_zero {d : ℕ} (x : Space d.succ) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (Metric.closedBall x r) ≠ 0

theorem Space.volume_closedBall_ne_top {d : ℕ} (x : Space d.succ) (r : ℝ) : MeasureTheory.volume (Metric.closedBall x r) ≠ ⊤

@[simp]

theorem Space.volume_metricBall_three : MeasureTheory.volume (Metric.ball 0 1) = ENNReal.ofReal (4 / 3 * Real.pi)

@[simp]

theorem Space.volume_metricBall_two : MeasureTheory.volume (Metric.ball 0 1) = ENNReal.ofReal Real.pi

@[simp]

theorem Space.volume_metricBall_two_real : MeasureTheory.volume.real (Metric.ball 0 1) = Real.pi

@[simp]

theorem Space.volume_metricBall_three_real : MeasureTheory.volume.real (Metric.ball 0 1) = 4 / 3 * Real.pi

B. Integrals over one-dimensional space

theorem Space.integral_one_dim_eq_integral_real {f : Space 1 → ℝ} : ∫ (x : Space 1), f x = ∫ (x : ℝ), f (oneEquiv.symm x)

C. Integrals over volume to spherical

theorem Space.integral_volume_eq_spherical {F : Type u_1} (d : ℕ) (f : Space d.succ → F) [NormedAddCommGroup F] [NormedSpace ℝ F] : ∫ (x : Space d.succ), f x = ∫ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂MeasureTheory.volume.toSphere.prod (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))

instance Space.instSFiniteElemRealIoiOfNatComapValMemSetVolume : MeasureTheory.SFinite (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)

D. Lower Lebesgue integral over volume to spherical

theorem Space.lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) : ∫⁻ (x : Space d.succ), f x = ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) ∂MeasureTheory.volume.toSphere.prod (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))

theorem Space.lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) : ∫⁻ (x : Space d.succ), f x = ∫⁻ (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)), f (↑x.2 • ↑x.1) * ENNReal.ofReal (↑x.2 ^ d) ∂MeasureTheory.volume.toSphere.prod (MeasureTheory.Measure.volumeIoiPow 0)