Integral of Positive Simple Function Well-Defined

From ProofWiki
Jump to navigation Jump to search


Let $\left({X, \Sigma, \mu}\right)$ be a measure space.

Let $f: X \to \R, f \in \mathcal{E}^+$ be a positive simple function.

Then the $\mu$-integral of $f$, $I_\mu \left({f}\right)$, is well-defined.

That is, for any two standard representations for $f$, say:

$\displaystyle f = \sum_{i \mathop = 0}^n a_i \chi_{E_i} = \sum_{j \mathop = 0}^m b_j \chi_{F_j}$

it holds that:

$\displaystyle \sum_{i \mathop = 0}^n a_i \mu \left({E_i}\right) = \sum_{j \mathop = 0}^m b_j \mu \left({F_j}\right)$


The sets $F_0, \ldots, F_m$ are pairwise disjoint, and:

$X = \displaystyle \bigcup_{j \mathop = 0}^m F_j$

From Characteristic Function of Disjoint Union, we have:

$\chi_X = \displaystyle \sum_{j \mathop = 0}^m \chi_{F_j}$

Remark that $\chi_X \left({x}\right) = 1$ for all $x \in X$, so that we have:

\(\displaystyle f\) \(=\) \(\displaystyle \sum_{i \mathop = 0}^n a_i \chi_{E_i} \cdot 1\)
\(\displaystyle \) \(=\) \(\displaystyle \sum_{i \mathop = 0}^n a_i \chi_{E_i} \left({\sum_{j \mathop = 0}^m \chi_{F_j} }\right)\)
\(\displaystyle \) \(=\) \(\displaystyle \sum_{i \mathop = 0}^n \sum_{j \mathop = 0}^m a_i \chi_{E_i} \chi_{F_j}\)
\(\displaystyle \) \(=\) \(\displaystyle \sum_{i \mathop = 0}^n \sum_{j \mathop = 0}^m a_i \chi_{E_i \cap F_j}\) Characteristic Function of Intersection: Variant 1

Repeating the argument with the $E_i$ and $F_j$ interchanged also yields:

$f = \displaystyle \sum_{j \mathop = 0}^m \sum_{i \mathop = 0}^n b_j \chi_{F_j \cap E_i}$

Now whenever $x \in E_i \cap F_j$, for some $i, j$, then since the $E_i$, $F_j$ are disjoint, we find:

$x \in E_{i'} \cap F_{j'}$ implies $i = i'$ and $j = j'$

Thus, evaluating both expressions for $f \left({x}\right)$ we find:

$a_i = f \left({x}\right) = b_j$

In conclusion, we have:

$a_i = b_j$

if $E_i \cap F_j \ne \varnothing$.

Furthermore, we have for all $i$ that:

$\displaystyle E_i = E_i \cap X = E_i \cap \left({\bigcup_{j \mathop = 0}^m F_j}\right) = \bigcup_{j \mathop = 0}^m \left({E_i \cap F_j}\right)$

by Intersection Distributes over Union: General Result.

Similarly, we obtain for all $j$:

$\displaystyle F_j = F_j \cap X = F_j \cap \left({\bigcup_{i \mathop = 0}^n E_i}\right) = \bigcup_{i \mathop = 0}^n \left({F_j \cap E_i}\right)$

With this knowledge, we compute:

\(\displaystyle \sum_{i \mathop = 0}^n a_i \mu \left({E_i}\right)\) \(=\) \(\displaystyle \sum_{i \mathop = 0}^n a_i \mu \left({\bigcup_{j \mathop = 0}^m \left({E_i \cap F_j}\right)}\right)\)
\(\displaystyle \) \(=\) \(\displaystyle \sum_{i \mathop = 0}^n a_i \sum_{j \mathop = 0}^m \mu \left({E_i \cap F_j}\right)\) Measure is Finitely Additive Function
\(\displaystyle \) \(=\) \(\displaystyle \sum_{i \mathop = 0}^n \sum_{j \mathop = 0}^m a_i \mu \left({E_i \cap F_j}\right)\) Summation is Linear
\(\displaystyle \) \(=\) \(\displaystyle \sum_{j \mathop = 0}^m \sum_{i \mathop = 0}^n b_j \mu \left({E_i \cap F_j}\right)\) If $a_i \ne b_j$ then $E_i \cap F_j = \varnothing$; $a_i \cdot 0 = b_j \cdot 0$
\(\displaystyle \) \(=\) \(\displaystyle \sum_{j \mathop = 0}^m b_j \sum_{i \mathop = 0}^n \mu \left({E_i \cap F_j}\right)\) Summation is Linear
\(\displaystyle \) \(=\) \(\displaystyle \sum_{j \mathop = 0}^m b_j \mu \left({\bigcup_{i \mathop = 0}^n \left({E_i \cap F_j}\right)}\right)\) Measure is Finitely Additive Function
\(\displaystyle \) \(=\) \(\displaystyle \sum_{j \mathop = 0}^m b_j \mu \left({F_j}\right)\)

Hence the result.