ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4916 on D3386: Unsigned basic Lebesgue integral
Subresult of R4915:
Formulation 0
Let $M = (\mathbb{R}, \mathcal{L}, \ell)$ be a D1744: Lebesgue measure space such that
(i) $f : \mathbb{R} \to [0, \infty]$ is a D5610: Unsigned basic Borel function on $M$
(ii) $a \in \mathbb{R} \setminus \{ 0 \}$ is a D993: Real number
Then
(1) \begin{equation} \int_{\mathbb{R}} f(x / a) \, \ell(d x) = |a| \int_{\mathbb{R}} f(x) \, \ell(d x) \end{equation}
(2) \begin{equation} \int_{\mathbb{R}} f(a x) \, \ell (d x) = \frac{1}{|a|} \int_{\mathbb{R}} f(x) \, \ell(d x) \end{equation}
Proofs
Proof 0
Let $M = (\mathbb{R}, \mathcal{L}, \ell)$ be a D1744: Lebesgue measure space such that
(i) $f : \mathbb{R} \to [0, \infty]$ is a D5610: Unsigned basic Borel function on $M$
(ii) $a \in \mathbb{R} \setminus \{ 0 \}$ is a D993: Real number
This result is a particular case of R4915: . $\square$