Corollary

— We maintain the hypotheses and notations of Th. 4. Let F' be a second μ-measurable fundamental domain. Let u be a function on X, with values in a Banach space or in $\overline{\mathbf{R}}$, invariant under H. Suppose that u is μ-integrable on F. Then u is μ-integrable on F' and

Since u and n are invariant under H, there exists a function v on X/H such that v o π coincides with nu on F and on F'. Then $n^{-1} \varphi_F(v \circ \pi) = \varphi_{F'} u, \quad n^{-1} \varphi_{F'}(v \circ \pi) = \varphi_{F'} u.$ By hypothesis, $n^{-1} \varphi_F(v \circ \pi)$ is $\mu$-integrable. By Th. 4, $v$ is $\lambda$-integrable, $\varphi_{F'} \mu$ is $\mu$-integrable, and

For the existence of $\mu$-measurable fundamental domains, see Exer. 12.