Volume of balls

Let E be a finite-dimensional normed ℝ-vector space equipped with a Haar measure μ. We prove that μ (Metric.ball 0 1) = (∫ (x : E), Real.exp (- ‖x‖ ^ p) ∂μ) / Real.Gamma (finrank ℝ E / p + 1) for any real number p with 0 < p, see MeasureTheory.measure_unitBall_eq_integral_div_gamma. We also prove the corresponding result to compute μ {x : E | g x < 1} where g : E → ℝ is a function defining a norm on E, see MeasureTheory.measure_lt_one_eq_integral_div_gamma.

Using these formulas, we compute the volume of the unit balls in several cases.

• MeasureTheory.volume_sum_rpow_lt / MeasureTheory.volume_sum_rpow_le: volume of the open and closed balls for the norm Lp over a real finite-dimensional vector space with 1 ≤ p. These are computed as volume {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) < r} and volume {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) ≤ r} since the spaces PiLp do not have a MeasureSpace instance.

• Complex.volume_sum_rpow_lt_one / Complex.volume_sum_rpow_lt: same as above but for complex finite-dimensional vector space.

• EuclideanSpace.volume_ball / EuclideanSpace.volume_closedBall : volume of open and closed balls in a finite-dimensional Euclidean space.

• InnerProductSpace.volume_ball / InnerProductSpace.volume_closedBall: volume of open and closed balls in a finite-dimensional real inner product space.

• Complex.volume_ball / Complex.volume_closedBall: volume of open and closed balls in ℂ.

theorem MeasureTheory.measure_unitBall_eq_integral_div_gamma {E : Type u_1} {p : ℝ} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hp : 0 < p) : μ (Metric.ball 0 1) = ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(Module.finrank ℝ E) / p + 1))

theorem MeasureTheory.measure_lt_one_eq_integral_div_gamma {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] [mE : MeasurableSpace E] [tE : TopologicalSpace E] [IsTopologicalAddGroup E] [BorelSpace E] [T2Space E] [ContinuousSMul ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {g : E → ℝ} (h1 : g 0 = 0) (h2 : ∀ (x : E), g (-x) = g x) (h3 : ∀ (x y : E), g (x + y) ≤ g x + g y) (h4 : ∀ {x : E}, g x = 0 → x = 0) (h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x) {p : ℝ} (hp : 0 < p) : μ {x : E | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(Module.finrank ℝ E) / p + 1))

theorem MeasureTheory.measure_le_eq_lt {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] [mE : MeasurableSpace E] [tE : TopologicalSpace E] [IsTopologicalAddGroup E] [BorelSpace E] [T2Space E] [ContinuousSMul ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {g : E → ℝ} (h1 : g 0 = 0) (h2 : ∀ (x : E), g (-x) = g x) (h3 : ∀ (x y : E), g (x + y) ≤ g x + g y) (h4 : ∀ {x : E}, g x = 0 → x = 0) (h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x) [Nontrivial E] (r : ℝ) : μ {x : E | g x ≤ r} = μ {x : E | g x < r}

theorem MeasureTheory.volume_sum_rpow_lt_one (ι : Type u_1) [Fintype ι] {p : ℝ} (hp : 1 ≤ p) : volume {x : ι → ℝ | ∑ i : ι, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))

theorem MeasureTheory.volume_sum_rpow_lt (ι : Type u_1) [Fintype ι] [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) : volume {x : ι → ℝ | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))

theorem MeasureTheory.volume_sum_rpow_le (ι : Type u_1) [Fintype ι] [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) : volume {x : ι → ℝ | (∑ i : ι, |x i| ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))

theorem Complex.volume_sum_rpow_lt_one (ι : Type u_1) [Fintype ι] {p : ℝ} (hp : 1 ≤ p) : MeasureTheory.volume {x : ι → ℂ | ∑ i : ι, ‖x i‖ ^ p < 1} = ENNReal.ofReal ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))

theorem Complex.volume_sum_rpow_lt (ι : Type u_1) [Fintype ι] [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) : MeasureTheory.volume {x : ι → ℂ | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ (2 * Fintype.card ι) * ENNReal.ofReal ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))

theorem Complex.volume_sum_rpow_le (ι : Type u_1) [Fintype ι] [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) : MeasureTheory.volume {x : ι → ℂ | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * Fintype.card ι) * ENNReal.ofReal ((Real.pi * Real.Gamma (2 / p + 1)) ^ Fintype.card ι / Real.Gamma (2 * ↑(Fintype.card ι) / p + 1))

theorem EuclideanSpace.volume_ball (ι : Type u_1) [Nonempty ι] [Fintype ι] (x : EuclideanSpace ℝ ι) (r : ℝ) : MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal (√Real.pi ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / 2 + 1))

theorem EuclideanSpace.volume_closedBall (ι : Type u_1) [Nonempty ι] [Fintype ι] (x : EuclideanSpace ℝ ι) (r : ℝ) : MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal (√Real.pi ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / 2 + 1))

theorem InnerProductSpace.volume_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] (x : E) (r : ℝ) : MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ Module.finrank ℝ E * ENNReal.ofReal (√Real.pi ^ Module.finrank ℝ E / Real.Gamma (↑(Module.finrank ℝ E) / 2 + 1))

theorem InnerProductSpace.volume_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] (x : E) (r : ℝ) : MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ Module.finrank ℝ E * ENNReal.ofReal (√Real.pi ^ Module.finrank ℝ E / Real.Gamma (↑(Module.finrank ℝ E) / 2 + 1))

theorem InnerProductSpace.volume_ball_of_dim_even {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {k : ℕ} (hk : Module.finrank ℝ E = 2 * k) (x : E) (r : ℝ) : MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ Module.finrank ℝ E * ENNReal.ofReal (Real.pi ^ k / ↑k.factorial)

theorem InnerProductSpace.volume_closedBall_of_dim_even {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {k : ℕ} (hk : Module.finrank ℝ E = 2 * k) (x : E) (r : ℝ) : MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ Module.finrank ℝ E * ENNReal.ofReal (Real.pi ^ k / ↑k.factorial)

theorem InnerProductSpace.volume_ball_of_dim_odd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {k : ℕ} (hk : Module.finrank ℝ E = 2 * k + 1) (x : E) (r : ℝ) : MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ Module.finrank ℝ E * ENNReal.ofReal (Real.pi ^ k * 2 ^ (k + 1) / ↑(Module.finrank ℝ E).doubleFactorial)

theorem InnerProductSpace.volume_closedBall_of_dim_odd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {k : ℕ} (hk : Module.finrank ℝ E = 2 * k + 1) (x : E) (r : ℝ) : MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ Module.finrank ℝ E * ENNReal.ofReal (Real.pi ^ k * 2 ^ (k + 1) / ↑(Module.finrank ℝ E).doubleFactorial)

@[simp]

theorem EuclideanSpace.volume_ball_fin_two (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ 2 * ENNReal.ofReal Real.pi

@[simp]

theorem EuclideanSpace.volume_closedBall_fin_two (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ 2 * ENNReal.ofReal Real.pi

@[simp]

theorem EuclideanSpace.volume_ball_fin_three (x : EuclideanSpace ℝ (Fin 3)) (r : ℝ) : MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ 3 * ENNReal.ofReal (Real.pi * 4 / 3)

@[simp]

theorem EuclideanSpace.volume_closedBall_fin_three (x : EuclideanSpace ℝ (Fin 3)) (r : ℝ) : MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ 3 * ENNReal.ofReal (Real.pi * 4 / 3)

@[simp]

theorem Complex.volume_ball (a : ℂ) (r : ℝ) : MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi

@[simp]

theorem Complex.volume_closedBall (a : ℂ) (r : ℝ) : MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi