Documentation

Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

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.

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 = 0x = 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 = 0x = 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))
@[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