The real volume of the unit ball

Mathlib computes the volume of a ball in a finite-dimensional real inner product space as an extended nonnegative real (InnerProductSpace.volume_ball). This file records the real volume of the unit ball in the form π ^ (d / 2) / Γ(d / 2 + 1), where d is the dimension, which is the form used in normalizing constants. It also shows that every finite-dimensional real inner product space has a closed ball of volume one about the origin, that a closed ball of radius r in a one-dimensional space has volume 2 * r, and that a disc of radius r in ℂ has real volume π * r ^ 2, so that a constant c on it has L² norm ‖c‖ r √π.

theorem TauCeti.volume_real_unitBall {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : MeasureTheory.volume.real (Metric.ball 0 1) = Real.pi ^ (↑(Module.finrank ℝ V) / 2) / Real.Gamma (↑(Module.finrank ℝ V) / 2 + 1)

The real volume of the unit ball of a real inner product space of dimension d is π ^ (d / 2) / Γ(d / 2 + 1).

theorem TauCeti.exists_volume_closedBall_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : ∃ (ρ : ℝ), 0 < ρ ∧ MeasureTheory.volume (Metric.closedBall 0 ρ) = 1

There is a closed ball about the origin of volume one.

theorem TauCeti.volume_real_closedBall_of_finrank_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (h : Module.finrank ℝ V = 1) (x : V) {r : ℝ} (hr : 0 ≤ r) : MeasureTheory.volume.real (Metric.closedBall x r) = 2 * r

In a one-dimensional real inner product space, a closed ball of radius r ≥ 0 has volume 2 * r.

theorem Complex.volume_real_ball (a : ℂ) {r : ℝ} (hr : 0 ≤ r) : MeasureTheory.volume.real (Metric.ball a r) = Real.pi * r ^ 2

A disc of radius r ≥ 0 in ℂ has real volume π * r ^ 2.

theorem Complex.eLpNorm_two_indicator_closedBall_const {E : Type u_1} [NormedAddCommGroup E] (a : ℂ) (c : E) {R : ℝ} (hR : 0 ≤ R) : MeasureTheory.eLpNorm ((Metric.closedBall a R).indicator fun (x : ℂ) => c) 2 MeasureTheory.volume = ‖c‖ₑ * ENNReal.ofReal (R * √Real.pi)

The L² norm of a constant c on the closed disc of radius R in ℂ is ‖c‖ R √π, the square root of the disc area π R² times ‖c‖.