English
For a finite-dimensional real vector space E with Haar measure μ, the measure of the unit ball B(0,1) equals a gamma-integral expression: μ(B(0,1)) = Γ-fraction involving dim(E) and p, times a normalizing factor.
Русский
Для конечномерного вещественного пространства E с мерами Хаара μ мера единичного шара B(0,1) равна гамма-интегралу, зависящему от размерности пространства.
LaTeX
$$$\\mu(B(0,1)) = \\mathrm{OFReal}\\left( \\frac{\\int_E e^{-\\|x\\|^p} \\, d\\mu(x)}{\\Gamma(\\mathrm{finrank}_\\mathbb{R} E / p + 1)} \\right)$$$
Lean4
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) = .ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma (finrank ℝ E / p + 1)) :=
by
obtain hE | hE := subsingleton_or_nontrivial E
·
rw [(Metric.nonempty_ball.mpr zero_lt_one).eq_zero, ← setIntegral_univ, Set.univ_nonempty.eq_zero,
integral_singleton, finrank_zero_of_subsingleton, Nat.cast_zero, zero_div, zero_add, Real.Gamma_one, div_one,
norm_zero, Real.zero_rpow hp.ne', neg_zero, Real.exp_zero, smul_eq_mul, mul_one, measureReal_def,
ofReal_toReal (measure_ne_top μ {0})]
· have : (0 : ℝ) < finrank ℝ E := Nat.cast_pos.mpr finrank_pos
have :
((∫ y in Set.Ioi (0 : ℝ), y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma ((finrank ℝ E) / p + 1)) *
(finrank ℝ E) =
1 :=
by
simp_rw [← Real.rpow_natCast _ (finrank ℝ E - 1), smul_eq_mul, Nat.cast_sub finrank_pos, Nat.cast_one]
rw [integral_rpow_mul_exp_neg_rpow hp (by linarith), sub_add_cancel,
Real.Gamma_add_one (ne_of_gt (by positivity))]
field_simp
rw [integral_fun_norm_addHaar μ (fun x => Real.exp (-x ^ p)), nsmul_eq_mul, smul_eq_mul, mul_div_assoc,
mul_div_assoc, mul_comm, mul_assoc, this, mul_one, ofReal_measureReal _]
exact ne_of_lt measure_ball_lt_top
