ThmDex – An index of mathematical definitions, results, and conjectures.
Translation invariance of unsigned basic Lebesgue integral
Formulation 0
Let $M = (\mathbb{R}^n, \mathcal{L}, \mu)$ be a D1744: Lebesgue measure space.
Let $f : \mathbb{R}^n \to [0, \infty]$ be a D313: Measurable function with respect to $M$.
Then \begin{equation} \forall \, y \in \mathbb{R}^n : \int_{\mathbb{R}^n} f(x + y) \, d \mu(x) = \int_{\mathbb{R}^n} f(x) \, d \mu(x) \end{equation}
Proofs
Proof 0
Let $M = (\mathbb{R}^n, \mathcal{L}, \mu)$ be a D1744: Lebesgue measure space.
Let $f : \mathbb{R}^n \to [0, \infty]$ be a D313: Measurable function with respect to $M$.
Let $y \in \mathbb{R}^n$. Let $E \in \mathcal{L}$ and let $\mathbb{I}_E$ be the indicator function for $E$ in $\mathbb{R}^n$. Results
(i) R2140: Translation of indicator function
(ii) R1242: Unsigned basic integral is compatible with measure
(iii) R1164: Translation invariance of Lebesgue measure

then imply \begin{equation} \begin{split} \int_{\mathbb{R}^n} \mathbb{I}_E(x + y) \, d \mu(x) & = \int_{\mathbb{R}^n} \mathbb{I}_{E - y}(x) \, d \mu(x) \\ & = \mu(E - y) = \mu(E) = \int_{\mathbb{R}^n} \mathbb{I}_E(x) \, d \mu(x) \end{split} \end{equation} This establishes the claim for measurable indicator functions $\mathbb{R}^n \to \{ 0, 1 \}$. The claim for unsigned functions $\mathbb{R}^n \to [0, \infty]$ then follows by applying the principles in [[[x,125]]]. $\square$