## Function integral

### Set

 context $\mathbb K = \overline{\mathbb R}\lor \mathbb C$ context $\langle X,\Sigma,\mu\rangle\in \mathrm{MeasureSpace}(X)$ definiendum $\int_X: (X\to \mathbb K)\to \mathbb K$ definiendum $\int_X\ f\ \mathrm d\mu:=\int_X\ (\mathrm{Re}f)^+\ \mathrm d\mu-\int_X\ (\mathrm{Re}f)^-\ \mathrm d\mu+i\ \left( \int_X\ (\mathrm{Im}f)^+\ \mathrm d\mu-\ \int_X\ (\mathrm{Im}f)^-\ \mathrm d\mu \right)$

Notice that the integral on the right hand side here is that for positive measurable numerical functions.