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

• Euclidean_space.volume_ball / Euclidean_space.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] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] (hp : 0 < p) : ↑↑μ (Metric.ball 0 1) = ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (↑(FiniteDimensional.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] [TopologicalAddGroup E] [BorelSpace E] [T2Space E] [ContinuousSMul ℝ E] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.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 (↑(FiniteDimensional.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] [TopologicalAddGroup E] [BorelSpace E] [T2Space E] [ContinuousSMul ℝ E] (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.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) : ↑↑MeasureTheory.volume {x : ι → ℝ | (Finset.sum Finset.univ fun (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 : ℝ) : ↑↑MeasureTheory.volume {x : ι → ℝ | (Finset.sum Finset.univ fun (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 : ℝ) : ↑↑MeasureTheory.volume {x : ι → ℝ | (Finset.sum Finset.univ fun (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 : ι → ℂ | (Finset.sum Finset.univ fun (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 : ι → ℂ | (Finset.sum Finset.univ fun (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 : ι → ℂ | (Finset.sum Finset.univ fun (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 Euclidean_space.volume_ball (ι : Type u_1) [Nonempty ι] [Fintype ι] (x : EuclideanSpace ℝ ι) (r : ℝ) : ↑↑MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal (Real.sqrt Real.pi ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / 2 + 1))

theorem Euclidean_space.volume_closedBall (ι : Type u_1) [Nonempty ι] [Fintype ι] (x : EuclideanSpace ℝ ι) (r : ℝ) : ↑↑MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ Fintype.card ι * ENNReal.ofReal (Real.sqrt 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 ^ FiniteDimensional.finrank ℝ E * ENNReal.ofReal (Real.sqrt Real.pi ^ FiniteDimensional.finrank ℝ E / Real.Gamma (↑(FiniteDimensional.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 ^ FiniteDimensional.finrank ℝ E * ENNReal.ofReal (Real.sqrt Real.pi ^ FiniteDimensional.finrank ℝ E / Real.Gamma (↑(FiniteDimensional.finrank ℝ E) / 2 + 1))

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