Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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:
```lean
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.
```lean
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`.
```lean
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.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>- Loading branch information
Showing
10 changed files
with
594 additions
and
62 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,138 @@ | ||
| /- | ||
| Copyright (c) 2023 Xavier Roblot. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Xavier Roblot | ||
| -/ | ||
| import Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup | ||
|
|
||
| /-! | ||
| # Integrals involving the Gamma function | ||
| In this file, we collect several integrals over `ℝ` or `ℂ` that evaluate in terms of the | ||
| `Real.Gamma` function. | ||
| -/ | ||
|
|
||
| open Real Set MeasureTheory MeasureTheory.Measure | ||
|
|
||
| section real | ||
|
|
||
| theorem integral_rpow_mul_exp_neg_rpow {p q : ℝ} (hp : 0 < p) (hq : - 1 < q) : | ||
| ∫ x in Ioi (0:ℝ), x ^ q * exp (- x ^ p) = (1 / p) * Gamma ((q + 1) / p) := by | ||
| calc | ||
| _ = ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * exp (-x)) := by | ||
| rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)), | ||
| abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))] | ||
| refine set_integral_congr measurableSet_Ioi (fun _ hx => ?_) | ||
| rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one] | ||
| _ = ∫ (x : ℝ) in Ioi 0, 1 / p * exp (-x) * x ^ (1 / p - 1 + q / p) := by | ||
| simp_rw [smul_eq_mul, mul_assoc] | ||
| refine set_integral_congr measurableSet_Ioi (fun _ hx => ?_) | ||
| rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx] | ||
| ring_nf | ||
| _ = (1 / p) * Gamma ((q + 1) / p) := by | ||
| rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)] | ||
| simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by field_simp; ring, ← integral_mul_left, | ||
| ← mul_assoc] | ||
|
|
||
| theorem integral_rpow_mul_exp_neg_mul_rpow {p q b : ℝ} (hp : 0 < p) (hq : - 1 < q) (hb : 0 < b) : | ||
| ∫ x in Ioi (0:ℝ), x ^ q * exp (- b * x ^ p) = | ||
| b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by | ||
| calc | ||
| _ = ∫ x in Ioi (0:ℝ), b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)) := by | ||
| refine set_integral_congr measurableSet_Ioi (fun _ hx => ?_) | ||
| rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul, | ||
| inv_mul_cancel, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, add_left_neg, | ||
| rpow_zero, one_mul, neg_mul] | ||
| all_goals positivity | ||
| _ = (b ^ p⁻¹)⁻¹ * ∫ x in Ioi (0:ℝ), b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) := by | ||
| rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (- x ^ p))) 0, | ||
| mul_zero, abs_eq_self.mpr ?_, smul_eq_mul] | ||
| all_goals positivity | ||
| _ = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by | ||
| rw [integral_mul_left, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc, | ||
| ← rpow_neg_one, ← rpow_mul, ← rpow_add] | ||
| congr; ring | ||
| all_goals positivity | ||
|
|
||
| theorem integral_exp_neg_rpow {p : ℝ} (hp : 0 < p) : | ||
| ∫ x in Ioi (0:ℝ), exp (- x ^ p) = Gamma (1 / p + 1) := by | ||
| convert (integral_rpow_mul_exp_neg_rpow hp neg_one_lt_zero) using 1 | ||
| · simp_rw [rpow_zero, one_mul] | ||
| · rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp))] | ||
|
|
||
| theorem integral_exp_neg_mul_rpow {p b : ℝ} (hp : 0 < p) (hb : 0 < b) : | ||
| ∫ x in Ioi (0:ℝ), exp (- b * x ^ p) = b ^ (- 1 / p) * Gamma (1 / p + 1) := by | ||
| convert (integral_rpow_mul_exp_neg_mul_rpow hp neg_one_lt_zero hb) using 1 | ||
| · simp_rw [rpow_zero, one_mul] | ||
| · rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp)), mul_assoc] | ||
|
|
||
| end real | ||
|
|
||
| section complex | ||
|
|
||
| theorem Complex.integral_rpow_mul_exp_neg_rpow {p q : ℝ} (hp : 1 ≤ p) (hq : - 2 < q) : | ||
| ∫ x : ℂ, ‖x‖ ^ q * rexp (- ‖x‖ ^ p) = (2 * π / p) * Real.Gamma ((q + 2) / p) := by | ||
| calc | ||
| _ = ∫ x in Ioi (0:ℝ) ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) := by | ||
| rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target] | ||
| simp_rw [Complex.norm_eq_abs, Complex.polardCoord_symm_abs, smul_eq_mul] | ||
| _ = (∫ x in Ioi (0:ℝ), x * |x| ^ q * rexp (-|x| ^ p)) * ∫ _ in Ioo (-π) π, 1 := by | ||
| rw [← set_integral_prod_mul, volume_eq_prod] | ||
| simp_rw [mul_one] | ||
| congr! 2; ring | ||
| _ = 2 * π * ∫ x in Ioi (0:ℝ), x * |x| ^ q * rexp (-|x| ^ p) := by | ||
| simp_rw [integral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter, | ||
| volume_Ioo, sub_neg_eq_add, ← two_mul, ENNReal.toReal_ofReal (by positivity : 0 ≤ 2 * π), | ||
| smul_eq_mul, mul_one, mul_comm] | ||
| _ = 2 * π * ∫ x in Ioi (0:ℝ), x ^ (q + 1) * rexp (-x ^ p) := by | ||
| congr 1 | ||
| refine set_integral_congr measurableSet_Ioi (fun x hx => ?_) | ||
| rw [abs_eq_self.mpr (le_of_lt (by exact hx)), rpow_add hx, rpow_one] | ||
| ring | ||
| _ = (2 * Real.pi / p) * Real.Gamma ((q + 2) / p) := by | ||
| rw [_root_.integral_rpow_mul_exp_neg_rpow (by linarith) (by linarith), add_assoc, | ||
| one_add_one_eq_two] | ||
| ring | ||
|
|
||
| theorem Complex.integral_rpow_mul_exp_neg_mul_rpow {p q b : ℝ} (hp : 1 ≤ p) (hq : - 2 < q) | ||
| (hb : 0 < b) : | ||
| ∫ x : ℂ, ‖x‖ ^ q * rexp (- b * ‖x‖ ^ p) = (2 * π / p) * | ||
| b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p) := by | ||
| calc | ||
| _ = ∫ x in Ioi (0:ℝ) ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (- b * |x.1| ^ p)) := by | ||
| rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target] | ||
| simp_rw [Complex.norm_eq_abs, Complex.polardCoord_symm_abs, smul_eq_mul] | ||
| _ = (∫ x in Ioi (0:ℝ), x * |x| ^ q * rexp (- b * |x| ^ p)) * ∫ _ in Ioo (-π) π, 1 := by | ||
| rw [← set_integral_prod_mul, volume_eq_prod] | ||
| simp_rw [mul_one] | ||
| congr! 2; ring | ||
| _ = 2 * π * ∫ x in Ioi (0:ℝ), x * |x| ^ q * rexp (- b * |x| ^ p) := by | ||
| simp_rw [integral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter, | ||
| volume_Ioo, sub_neg_eq_add, ← two_mul, ENNReal.toReal_ofReal (by positivity : 0 ≤ 2 * π), | ||
| smul_eq_mul, mul_one, mul_comm] | ||
| _ = 2 * π * ∫ x in Ioi (0:ℝ), x ^ (q + 1) * rexp (-b * x ^ p) := by | ||
| congr 1 | ||
| refine set_integral_congr measurableSet_Ioi (fun x hx => ?_) | ||
| rw [abs_eq_self.mpr (le_of_lt (by exact hx)), rpow_add hx, rpow_one] | ||
| ring | ||
| _ = (2 * π / p) * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p) := by | ||
| rw [_root_.integral_rpow_mul_exp_neg_mul_rpow (by linarith) (by linarith) hb, add_assoc, | ||
| one_add_one_eq_two] | ||
| ring | ||
|
|
||
| theorem Complex.integral_exp_neg_rpow {p : ℝ} (hp : 1 ≤ p) : | ||
| ∫ x : ℂ, rexp (- ‖x‖ ^ p) = π * Real.Gamma (2 / p + 1) := by | ||
| convert (integral_rpow_mul_exp_neg_rpow hp (by linarith : (-2:ℝ) < 0)) using 1 | ||
| · simp_rw [norm_eq_abs, rpow_zero, one_mul] | ||
| · rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))] | ||
| ring | ||
|
|
||
| theorem Complex.integral_exp_neg_mul_rpow {p b : ℝ} (hp : 1 ≤ p) (hb : 0 < b) : | ||
| ∫ x : ℂ, rexp (- b * ‖x‖ ^ p) = π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) := by | ||
| convert (integral_rpow_mul_exp_neg_mul_rpow hp (by linarith : (-2:ℝ) < 0)) hb using 1 | ||
| · simp_rw [norm_eq_abs, rpow_zero, one_mul] | ||
| · rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))] | ||
| ring | ||
|
|
||
| end complex |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,49 @@ | ||
| /- | ||
| Copyright (c) 2023 Xavier Roblot. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Xavier Roblot | ||
| -/ | ||
| import Mathlib.MeasureTheory.Constructions.Pi | ||
| import Mathlib.MeasureTheory.Constructions.Prod.Integral | ||
|
|
||
| /-! | ||
| # Integration with respect to a finite product of measures | ||
| -/ | ||
|
|
||
| open BigOperators Fintype MeasureTheory MeasureTheory.Measure | ||
|
|
||
| theorem MeasureTheory.integral_finset_prod_eq_prod' {E : Type*} {n : ℕ} (f : (Fin n) → E → ℝ) | ||
| [MeasureSpace E] [SigmaFinite (volume : Measure E)] : | ||
| ∫ x : (Fin n) → E, ∏ i, f i (x i) = ∏ i, ∫ x, f i x := by | ||
| induction n with | ||
| | zero => | ||
| simp only [Nat.zero_eq, volume_pi, Finset.univ_eq_empty, Finset.prod_empty, integral_const, | ||
| pi_empty_univ, ENNReal.one_toReal, smul_eq_mul, mul_one, pow_zero] | ||
| | succ n n_ih => | ||
| calc | ||
| _ = ∫ x : E × (Fin n → E), f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i) := by | ||
| rw [volume_pi, ← ((measurePreserving_piFinSuccAboveEquiv | ||
| (fun _ => (volume : Measure E)) 0).symm).integral_comp'] | ||
| simp_rw [MeasurableEquiv.piFinSuccAboveEquiv_symm_apply, Fin.insertNth_zero', | ||
| Fin.prod_univ_succ, Fin.cons_zero, Fin.cons_succ] | ||
| rfl | ||
| _ = (∫ x, f 0 x) * ∏ i : Fin n, ∫ (x : E), f (Fin.succ i) x := by | ||
| rw [← n_ih, ← integral_prod_mul, volume_eq_prod] | ||
| _ = ∏ i, ∫ x, f i x := by rw [Fin.prod_univ_succ] | ||
|
|
||
| theorem MeasureTheory.integral_finset_prod_eq_prod {E : Type*} (ι : Type*) [Fintype ι] | ||
| (f : ι → E → ℝ) [MeasureSpace E] [SigmaFinite (volume : Measure E)] : | ||
| ∫ x : ι → E, ∏ i, f i (x i) = ∏ i, ∫ x, f i x := by | ||
| let e := (equivFin ι) | ||
| let p := measurePreserving_piCongrLeft (fun _ => (volume : Measure E)) e | ||
| rw [volume_pi, ← (p.symm).integral_comp', Fintype.prod_equiv e _ (fun j => ∫ x, f (e.symm j) x) | ||
| (fun _ => by simp_rw [e.symm_apply_apply]), ← integral_finset_prod_eq_prod' | ||
| (fun j => f (e.symm j))] | ||
| congr! | ||
| rw [Fintype.prod_equiv e] | ||
| exact fun _ => by simp [Equiv.symm_apply_apply]; rfl | ||
|
|
||
| theorem MeasureTheory.integral_finset_prod_eq_pow {E : Type*} (ι : Type*) [Fintype ι] (f : E → ℝ) | ||
| [MeasureSpace E] [SigmaFinite (volume : Measure E)] : | ||
| ∫ x : ι → E, ∏ i, f (x i) = (∫ x, f x) ^ (card ι) := by | ||
| rw [integral_finset_prod_eq_prod, Finset.prod_const, Fintype.card] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.