Commit 2023-12-07 17:41 f24e05a2

feat: Compute volume of balls of higher dimension for Lp norms (#8030) We give a formula measure_unitBall_eq_integral_div_gamma for computing the volume of the unit ball in a normed finite dimensional ℝ-vector space E with an Haar measure:

theorem measure_unitBall_eq_integral_div_gamma {E : Type*} {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 (finrank ℝ E / p + 1))

We also provide a theorem measure_lt_one_eq_integral_div_gamma to compute the volume of the ball {x : E | g x < 1} for a function g : E → ℝ defining a norm.

theorem measure_lt_one_eq_integral_div_gamma {E : Type*}
    [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] [mE : MeasurableSpace E]
    [tE : TopologicalSpace E] [TopologicalAddGroup E] [BorelSpace E] [T2Space E]
    [ContinuousSMul ℝ E] (μ : Measure E) [IsAddHaarMeasure μ]
    {g : E → ℝ} (hg0 : g 0 = 0) (hgn : ∀ x, g (- x) = g x) (hgt : ∀ x y, g (x + y) ≤ g x + g y)
    (hgs : ∀ {x}, g x = 0 → x = 0) (hns :  ∀ r x, 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 (finrank ℝ E / p + 1))

This provides a way to compute the volume of the unit ball for the norms L_p for 1 ≤ p in any dimension over the reals MeasureTheory.volume_sum_rpow_lt_one and the complex Complex.volume_sum_rpow_lt_one.

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

From these, we deduce the volume of balls in several situations.

Other significant changes include:

• Adding MeasurePreserving.integral_comp': when the theorem MeasurePreserving.integral_comp is used with f a measurable equiv, it is necessary to specify that it is a measurable embedding although it is trivial in this case. This version bypasses this hypothesis
• Proof of volume computations of the unit ball in ℂ and in EuclideanSpace ℝ (Fin 2) which are now done with the methods of the file VolumeOfBalls have been moved to this file.