Proof of The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions

Throughout, $X$, $\mathcal{F}$, $\mathcal{S}^{+}$, $\mathcal{M}^{+}$, $\mathrm{Meas}=\mathrm{Meas}(X,\mathcal{F};\mathbb{R},\mathcal{B}(\mathbb{R}))$, $\mathbb{R}^{X}$, $\mathbb{R}$, $[0,\infty]$ and $[-\infty,\infty]$ with their operations and orders, and $M$ are parameters, all but $M$ sets; each clause is expressed by a formula in three distinct variables called by the letters of the clause, in which values $F(u)$, $u\cdot v$ and uniquely described sets are named, each only where the conjuncts or antecedents before it make it exist, so that the formula is read as a formula tree (Formula Trees with Values: Syntax, Two Readings, and Definedness (i)) that uses its values properly (Formula Trees with Values: Syntax, Two Readings, and Definedness (vi)) and is predicative by The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative (iii) and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i); the sum and the difference are the predicative formulas $\Sigma(D,h,r)$ of Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (vii), second form, for $+$ on $[0,\infty]$ (a commutative monoid by Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i)), saying that $D$ is finite, $h$ is a map $h:D\to[0,\infty]$ and $r=\sum_{c\in D}h(c)$, and $\Delta(a,b,r)$ of Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (i), saying that $a,b\in\mathbb{R}$ and $r=a-b$; and formulas are moved to the positions $i,j,k$, which may coincide, or to other variables or parameters, by Renaming and Substituting Variables in Predicative Formulas (i) and Renaming and Substituting Variables in Predicative Formulas (iii).

The simple integral. Let $\Phi_{S}(m,s,r)$ be

$$m:\mathcal{F}\to[0,\infty]\ \wedge\ s\in\mathcal{S}^{+}\ \wedge\ \exists D\,\exists h\,\Bigl(\forall c\,\bigl(c\in D\Leftrightarrow\exists a\,(a\in X\wedge(a,c)\in s)\bigr)\wedge\Sigma(D,h,r)\wedge\forall c\,\bigl(c\in D\Rightarrow h(c)=c\cdot m(s^{-1}(\{c\}))\bigr)\Bigr),$$

where, inside the consequent of $c\in D\Rightarrow\dots$, $s^{-1}(\{c\})$ is named as the set $w$ with $\forall a\,(a\in w\Leftrightarrow(a\in X\wedge(a,c)\in s))$, so that $h(c)$ and $c\cdot m(w)$ are read only for $c\in D$. There $s$ is a map $X\to[0,\infty)$, $D=s[X]$ and $s^{-1}(\{c\})\in\mathcal{F}$ (Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv)), so these values exist. Thus $\Phi_{S}$ says that $m$ is a map $\mathcal{F}\to[0,\infty]$, $s\in\mathcal{S}^{+}$ and $r$ is the sum over $s[X]$ of the map $c\mapsto c\cdot m(s^{-1}(\{c\}))$, which exists by Maps and Relations Given by Formulas (i); so $I_{m}(s)$ exists for every such $m$, and $r=I_{m}(s)$. This proves (i).

The integral of a nonnegative function. Let $\sigma(S,r)$ be the formula of Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (i) for $[-\infty,\infty]$ with its order, a partial order by Order and Suprema in the Extended Real Line (i), and let $\Phi_{N}(m,g,r)$ be

$$m:\mathcal{F}\to[0,\infty]\ \wedge\ g\in\mathcal{M}^{+}\ \wedge\ \exists S\,\Bigl(\forall v\,\Bigl(v\in S\Leftrightarrow\exists s\,\bigl(s\in\mathcal{S}^{+}\wedge\forall x\,(x\in X\Rightarrow s(x)\le g(x))\wedge\Phi_{S}(m,s,v)\bigr)\Bigr)\wedge\sigma(S,r)\Bigr),$$

with $s(x)$ and $g(x)$ read after the guards $s\in\mathcal{S}^{+}$, $g\in\mathcal{M}^{+}$ and $x\in X$. Where the first two conjuncts hold, $\{I_{m}(s):s\in\mathcal{S}^{+},\ s\le g\}$ is a subclass of $[0,\infty]$ given by a predicative condition, by (i), hence a set (Sets and Maps: Ordinary Notation (iii)), and by extensionality the only $S$ satisfying the first part of the bracket. By Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (i) and Order and Suprema in the Extended Real Line (iii), $\sigma(S,r)$ then says that $r$ is its supremum, that is, $r=\int g\,dm$. This proves (ii).

The integral of an integrable function. Let $\pi(f,g)$ and $\eta(f,g)$ be the predicative formulas of The Functions f ↦ f⁺ and f ↦ f⁻ on the Real-Valued Functions on a Set, and a Predicative Form of g = f⁺ and g = f⁻ (ii), expressing "$f\in\mathbb{R}^{X}$ and $g=f^{+}$" and "$f\in\mathbb{R}^{X}$ and $g=f^{-}$", and let

$$\Phi_{I}(m,f,r):\quad m:\mathcal{F}\to[0,\infty]\wedge f\in\mathrm{Meas}\wedge\exists g\,\exists h\,\exists a\,\exists b\,\bigl(\pi(f,g)\wedge\eta(f,h)\wedge\Phi_{N}(m,g,a)\wedge\Phi_{N}(m,h,b)\wedge\Delta(a,b,r)\bigr).$$

For a map $m:\mathcal{F}\to[0,\infty]$ and $f\in\mathrm{Meas}$, the formulas force $g=f^{+}$ and $h=f^{-}$, which lie in $\mathcal{M}^{+}$ by Arithmetic of Measurable Real- and [0,∞]-Valued Maps (i) and Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vii), and then $a=\int f^{+}dm$ and $b=\int f^{-}dm$ by (ii). These lie in $\mathbb{R}$ exactly when they are below $\infty$ (Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii)), that is, exactly when $f\in\mathcal{L}^{1}(m)$, and then $r=a-b=\int f\,dm$. So $\Phi_{I}$ expresses the condition of (iii).

The integral against a finite signed measure. Let $\nu\in M$, a map $\nu:\mathcal{F}\to\mathbb{R}$ (Finite Signed Measures (i)). Consider

$$\Psi(\nu,f,r):\quad\nu\in M\wedge\exists P\,\exists p\,\exists q\,\exists a\,\exists b\,\bigl(H(\nu,P)\wedge J^{+}(\nu,P,p)\wedge J^{-}(\nu,P,q)\wedge\Phi_{I}(p,f,a)\wedge\Phi_{I}(q,f,b)\wedge\Delta(a,b,r)\bigr),$$

where $H(\nu,P)$ says that $P\in\mathcal{F}$, that $0\le\nu(A)$ for every $A\in\mathcal{F}$ with $A\subseteq P$ and that $\nu(A)\le0$ for every $A\in\mathcal{F}$ with $A\subseteq X\setminus P$; $J^{+}(\nu,P,p)$ says that $p$ is a map $p:\mathcal{F}\to[0,\infty]$ with $p(A)=\nu(A\cap P)$ for every $A\in\mathcal{F}$; and $J^{-}(\nu,P,q)$ says that $q$ is a map $q:\mathcal{F}\to[0,\infty]$ with $\Delta(0,\nu(A\setminus P),q(A))$ for every $A\in\mathcal{F}$. The sets $A\cap P$ and $A\setminus P$ are named by their elements, and $\nu(A\cap P)$, $\nu(A\setminus P)$, $p(A)$ and $q(A)$ are read only after the guards $\nu\in M$, $P\in\mathcal{F}$ (the first conjunct of $H$), $A\in\mathcal{F}$ and "$p$, respectively $q$, is a map on $\mathcal{F}$", where they exist (Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (ix), Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (x)).

For $\nu\in M$, $H(\nu,P)$ says that $P$ is a Hahn set for $\nu$; then $J^{+}$ and $J^{-}$ hold exactly for $p=\nu^{+}$ and $q=\nu^{-}$, the Jordan parts of Hahn and Jordan Decompositions of a Finite Signed Measure (ii), and by (iii), applied to these measures, the bracket says that $f\in\mathcal{L}^{1}(\nu^{+})$, $f\in\mathcal{L}^{1}(\nu^{-})$ and $r=\int f\,d\nu^{+}-\int f\,d\nu^{-}$. Under dependent choice $\nu$ has a Hahn set (Hahn and Jordan Decompositions of a Finite Signed Measure (i)), and none of this depends on which one. A function in $\mathcal{L}^{1}(\nu^{+})$ is measurable (Integrable Functions and Their Lebesgue Integral (ii)), and for measurable $f$, Properties of the Total Variation: a Finite Measure, the Jordan Decomposition, Linear Combinations, the Total Variation Norm, and Integrability (viii) gives $f\in\mathcal{L}^{1}(|\nu|)$, that is $f\in\mathcal{L}^{1}(\nu)$ (Integrable Functions and the Integral with Respect to a Finite Signed Measure (i)), if and only if $f\in\mathcal{L}^{1}(\nu^{+})$ and $f\in\mathcal{L}^{1}(\nu^{-})$; and then $r=\int f\,d\nu$ by Integrable Functions and the Integral with Respect to a Finite Signed Measure (ii). So $\Psi$ holds exactly when $\nu\in M$, $f\in\mathcal{L}^{1}(\nu)$ and $r=\int f\,d\nu$, which proves (iv).