Riemannian volume is the radon measure of the riemannian density

Given: A Riemannian manifold and countable choice.

The riemannian volume density is coordinate independent: The local Riemannian volume densities glue to a positive smooth density independent of coordinates.

The riemannian distance topology is the manifold topology: The topology of $d_g$ is the manifold topology on every connected Riemannian manifold.

Riemannian volume of a compactly supported smooth density: Assume countable choice. For smooth compactly supported $f$, define ${\int }_{M}f{\mu }_g$ by the intrinsic smooth density integral. More generally every compactly supported signed smooth density $\sigma$ has its existing intrinsic integral, independently of a Riemannian metric. lem-the-riemannian-volume-density-is-coordinate-independent makes $f{\mu }_g$ a smooth compactly supported density. Apply def-integral-of-a-compactly-supported-smooth-density and thm-density-integration-is-defined-without-an-orientation; def-countable-choice is inherited precisely at chart-partition selection. In a chart the summand is the integral of the partition-weighted coefficient $f\sqrt{\det G}$. On a zero-manifold it is the finite sum of scalar density values, and empty support gives zero. No orientation is required.

Positive smooth densities give Radon volume: If $r$ is a finite-valued positive smooth density, ${\mu }_r$ is finite on compact sets, locally finite, sigma-finite, and a regular Borel measure, hence Radon. Its completion is denoted $(M,\overline{\mathcal{B}(M)},{\bar{\mu }}_r)$ and is not identified with its Borel domain.

Measurable integration extends smooth density integration: For a nonnegative Borel $f:M\to [0,\mathrm{\infty }]$ and any chart partition $(x_i,{\phi }_i)$, ${\int }_{M}fd{\mu }_r={\sum }_i{\int }_{x_i(U_i)}({\phi }_{i}fr{)}_{x_i}d{\lambda }_n,$ with values in $[0,\mathrm{\infty }]$ and all zero-times-infinity products equal to zero. For positive smooth $r$ and compactly supported smooth real $f$, this equals the smooth density integral ${\int }_{M}fr$. For real or complex $f\in L^1({\mu }_r)$ the same chart formula holds, interpreted by real and imaginary positive and negative parts; the series converges absolutely. On the completion, nonnegative measurable functions and real or complex $L^1$ functions have Borel representatives modulo completed null sets, and the formulas are applied to those representatives.

The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$): The Axiom of Countable Choice, written ${\mathrm{A}\mathrm{C}}_{\omega }$, is the following statement. > For every family $(X_n{)}_{n\in \mathbb{N}}$ of nonempty sets indexed by > $\mathbb{N}$ there is a function $f$ with domain $\mathbb{N}$ such that > $f(n)\in X_n$ for every $n\in \mathbb{N}$. Equivalently, in the vocabulary of def-choice-function: every at most countable family of nonempty sets (def-countable) has a choice function.