English
For nonempty index set ι, p ≥ 1, the volume of the Lp-sphere with radius r equals r^{card ι} times a gamma-based constant depending on π and Gamma(… ).
Русский
Объем сферы Lp с радиусом r равен r^{card ι} умноженное на гамма-константу, зависящую от π и гамма-функции.
LaTeX
$$$\mathrm{volume}\{x : x_i \in \mathbb{R}, \sum_i |x_i|^p < r^p\} = r^{2|ι|} \Gamma(\cdots)$$$
Lean4
theorem volume_sum_rpow_le [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₁ : 0 < p := by
linarith
-- We collect facts about `Lp` norms that will be used in `measure_lt_one_eq_integral_div_gamma`
have eq_norm := fun x : ι → ℂ =>
(PiLp.norm_eq_sum (p := .ofReal p) (f := x) ((toReal_ofReal (le_of_lt h₁)).symm ▸ h₁))
simp_rw [toReal_ofReal (le_of_lt h₁)] at eq_norm
have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ENNReal.ofReal_one ▸ (ofReal_le_ofReal hp))
have nm_zero := norm_zero (E := PiLp (.ofReal p) (fun _ : ι => ℂ))
have eq_zero := fun x : ι → ℂ => norm_eq_zero (E := PiLp (.ofReal p) (fun _ : ι => ℂ)) (a := x)
have nm_neg := fun x : ι → ℂ => norm_neg (E := PiLp (.ofReal p) (fun _ : ι => ℂ)) x
have nm_add := fun x y : ι → ℂ => norm_add_le (E := PiLp (.ofReal p) (fun _ : ι => ℂ)) x y
simp_rw [eq_norm] at eq_zero nm_zero nm_neg nm_add
have nm_smul := fun (r : ℝ) (x : ι → ℂ) => norm_smul_le (β := PiLp (.ofReal p) (fun _ : ι => ℂ)) r x
simp_rw [eq_norm] at nm_smul
rw [measure_le_eq_lt _ nm_zero (fun x ↦ nm_neg x) (fun x y ↦ nm_add x y) (eq_zero _).mp (fun r x => nm_smul r x),
Complex.volume_sum_rpow_lt _ hp]
