English
For a finite index set ι with a parameter p ≥ 1, the volume of the set {x : (∑|x_i|^p)^{1/p} < r} equals r^{card ι} times a gamma-based constant depending on p and the dimension.
Русский
Для конечного множества индексов ι и параметра p ≥ 1 объем множества {x : (∑ |x_i|^p)^{1/p} < r} равен r^{card ι} умноженное на константу, зависящую от p и размерности.
LaTeX
$$$\mathrm{volume}\{x:\; \sum_i |x_i|^p < r^p\} = (r^p)^{|\iota|/p} \Gamma(\cdots)^{-1}$$$
Lean4
theorem volume_sum_rpow_lt [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) :
volume {x : ι → ℂ | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} =
(.ofReal r) ^ (2 * card ι) * .ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * card ι / p + 1)) :=
by
have h₁ (x : ι → ℂ) : 0 ≤ ∑ i, ‖x i‖ ^ p := by positivity
have h₂ : ∀ x : ι → ℂ, 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) := fun x => rpow_nonneg (h₁ x) _
obtain hr | hr := le_or_gt r 0
· have : {x : ι → ℂ | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} = ∅ :=
by
ext x
refine ⟨fun hx => ?_, fun hx => hx.elim⟩
exact not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)
rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
· rw [← Complex.volume_sum_rpow_lt_one _ hp, ← ENNReal.ofReal_pow (le_of_lt hr)]
convert addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℂ | ∑ i, ‖x i‖ ^ p < 1} using 2
·
simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply, norm_smul,
mul_rpow (norm_nonneg _) (norm_nonneg _), Real.norm_eq_abs, abs_inv, inv_rpow (abs_nonneg _), ← Finset.mul_sum,
abs_eq_self.mpr (le_of_lt hr), inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ←
rpow_lt_rpow_iff (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul (h₁ _),
div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
·
simp_rw [finrank_pi_fintype ℝ, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul, mul_comm,
Fintype.card]
