EDIT: TL;DR version - What is the role of the "measurable function" predicate in the definition of Lebesgue integrability? If the integrals of the positive and negative pieces are finite, that should be enough, right?
So I'm working on a definition of the Lebesgue integral for Metamath, and I'd like some feedback on the correctness of these definitions. Most books/articles separate these definitions by pages of text and go back and amend their definitions as they go, which is not something I can do, so I just want to make sure that I am understanding everything correctly.
$$\begin{align}\lambda^*:A\in{\cal P}(\Bbb R)\mapsto \inf\Big\{&\sum_{n\in\Bbb N}(f_2(n)-f_1(n))\,\Big|\ f:\Bbb N\to\Bbb R\times\Bbb R:\\ &\big(\forall n\in\Bbb N\ f_1(n)<f_2(n)\ \wedge\ A\subset\bigcup_{n\in\Bbb N}(f_1(n),f_2(n))\big)\Big\} \end{align}$$
$$\lambda=\lambda^*\restriction \{A\subseteq\Bbb R\ |\ \forall B\subseteq\Bbb R\,(\lambda^*(B)\in\Bbb R\to\lambda^*(B)=\lambda^*(B\cap A)+\lambda^*(B\setminus A))\}$$
$$\alpha_0=\{\langle {\Bbb R}\times\{0\},0\rangle\}$$ $$\alpha_{n+1}=\{\langle g+x\,{\bf 1}_A,\alpha_n(g)+x\lambda(A)\rangle\mid g\in{\rm dom}\ \alpha_n,x\in\Bbb R^+,A\in{\rm dom}\ \lambda\}$$ $${\textstyle\int_1}=\bigcup_{n\in\Bbb N_0}\alpha_n$$
$${\textstyle\int_2}:(f:\Bbb R\to[0,\infty])\mapsto\sup\{{\textstyle\int_1}(g)\mid g\in{\rm dom}\ {\textstyle\int_1}:\forall x\in\Bbb R\ g(x)\le f(x)\}$$
$$\int_Af(x)\,dx=\sum_{k=0}^3i^k{\textstyle\int_2}\big(x\in\Bbb R\mapsto\max(\Re\big[f(x)i^{-k}\big],0)\cdot{\bf 1}_A(x)\big)$$
With a few light modifications for readability, that's exactly what my definition is going to be. In words: $\lambda^*$ is the Lebesgue outer measure, which is the infimum of the total length of all countable collections of intervals that cover $A$. Technical points: the collection uses open intervals, and they are required to be nonempty. Also, by "countable" I mean "denumerable" (no finite collections allowed). Thus, for example, $0$ is never in that set. But since it is an infimum, this is probably not an issue. Note that the infinite sum may possibly be $+\infty$; this is handled correctly (it is really the supremum of the partial sums over the extended reals, although I didn't write that above).
$\lambda$ is the Lebesgue measure, which is just the outer measure restricted to those sets which split any other set into disjoint pieces that add up to the whole. Technical points: we can only do this for those sets whose outer measure is finite, or else the addition is undefined (addition is not defined on the extended reals). I think this should still give the same result as if the quantifier ranged over all sets (which is the usual way of stating this). We write "$A$ is measurable" as "$A\in{\rm dom}\ \lambda$".
The $\alpha$ functions are a recursive definition of the Lebesgue integral over simple functions. All the $\alpha$ functions, as well as $\int_1$ and $\int_2$, are "integration" functions: they map functions (with domain $\Bbb R$ and range $\Bbb [0,\infty]$) to real numbers. I had to write out the $\alpha$ functions explicitly as sets of ordered pairs here. $\alpha_0$ has a singleton domain (the zero function) and maps it to zero; $\alpha_{n+1}$ is the collection of all function-value pairs formed by taking a function $g$ from $\alpha_n$, a positive real coefficient $x$, and a measurable set $A$, and forming the new function $z\in\Bbb R\mapsto g(z)+{\rm if}(z\in A,x,0)$ and giving it the value $\alpha_n(g)+x\lambda(A)$. Since the coefficient is strictly positive, the only time $\alpha_{n+1}$ and $\alpha_n$ use the same function is when the set $A$ is empty, in which case $\lambda(A)=0$ and the functions agree. Thus the $\alpha$ functions are compatible and their union $\int_1$ is the desired simple function integrator.
$\int_2$ is an integrator over nonnegative extended real functions; it is the supremum of all simple functions less than it. Technical note: this can be $+\infty$ if the function is bounded away from zero or takes the value $+\infty$ (which is allowed) on a set of positive measure.
The final full integral (written in the usual notation) is just the sum of $\int_2$ evaluated at the positive and negative real and imaginary pieces of the function, and with a region limiter tacked on for convenience.
Comments about this setup are welcome. But I also have a question: nowhere above was the concept of integrability mentioned. Obviously there will be an issue if any of the four $\int_2$ integrals evaluates to $\infty$ (recall that addition is not defined for $\pm\infty$), but other than that in what ways can this definition be misused? In particular, I see no reason for the concept of a "measurable function" to be needed; all of the expressions are perfectly well-defined for a non-measurable function, unless I am missing something. Is there some "basic property" that is absolutely essential that only works for measurable functions? And if you have a measurable function and all four integrals are finite, are we clear to call the function "(Lebesgue) integrable"?