Riemannian volume

DefinitionNormalized Hausdorff measure#✓fully proved

Let \(n\) be a natural number and let \(X\) be an extended metric space with its Borel \(\sigma\)-algebra. The normalized \(n\)-dimensional Hausdorff measure of \(X\) is the measure \(\frac{\omega_n}{2^n} \mathcal{H}^n\), where \(\omega_n\) is the Lebesgue volume of the open unit ball of the Euclidean space \(\mathbb{R}^n\) and \(\mathcal{H}^n\) is the unnormalized \(n\)-dimensional Hausdorff measure, in which a set of diameter \(r\) has content \(r^n\).

With this normalization it agrees with Lebesgue measure on \(\mathbb{R}^n\) (classically, by the isodiametric inequality); the case \(n = 1\) is checked by the computation of the Riemannian volume of the real line.

def normalizedHausdorffMeasure (n : ℕ) (X : Type*) [EMetricSpace X] [MeasurableSpace X]
    [BorelSpace X] : Measure X :=
  (volume (ball (0 : EuclideanSpace ℝ (Fin n)) 1) / 2 ^ n) • μH[n]

Used by 2

Used byRiemannian volume · The Riemannian volume of the real line is Lebesgue measure

DefinitionRiemannian volume#✓fully proved

Let \(E\) be a finite-dimensional real normed space, let \(I\) be a model with corners on \(E\), and let \(M\) be a \(C^\infty\) manifold modeled on \(I\), so that \(M\) has dimension \(n = \dim_{\mathbb{R}} E\). Suppose that \(M\) carries a \(C^\infty\) Riemannian metric and an extended metric equal to the Riemannian distance (the infimum of the lengths of \(C^1\) paths), and is given its Borel \(\sigma\)-algebra. The Riemannian volume of \(M\) is the normalized \(n\)-dimensional Hausdorff measure of \(M\).

The manifold and Riemannian hypotheses are not used in the formula; they tie the dimension to the model of \(M\) and restrict the definition to the setting in which, classically, this measure is the Riemannian volume, given in charts by the density \(\sqrt{\det(g_{ij})}\) against Lebesgue measure.

@[nolint unusedArguments]
def riemannianVolume [FiniteDimensional ℝ E] (I : ModelWithCorners ℝ E H) (M : Type*)
    [EMetricSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
    [RiemannianBundle (fun x : M ↦ TangentSpace I x)]
    [IsContMDiffRiemannianBundle I ∞ E (fun x : M ↦ TangentSpace I x)]
    [IsRiemannianManifold I M] [MeasurableSpace M] [BorelSpace M] : Measure M :=
  normalizedHausdorffMeasure (finrank ℝ E) M

Uses 1 · Used by 1

Statement usesNormalized Hausdorff measure

Used byThe Riemannian volume of the real line is Lebesgue measure

TheoremThe Riemannian volume of the real line is Lebesgue measure#✓fully proved

The Riemannian volume of the real line \(\mathbb{R}\), with its standard Riemannian metric (the usual inner product on each tangent space) and with its usual distance, which is the Riemannian distance, is Lebesgue measure.

This is a normalization check of the Riemannian volume in dimension one.

theorem riemannianVolume_real : riemannianVolume 𝓘(ℝ, ℝ) ℝ = volume

Uses 2

Statement usesRiemannian volume

Proof usesNormalized Hausdorff measure

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.