Proof of A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals

Auxiliary formulas. Let $\psi_{U}(a,b,f,P,z)$ and $\psi_{L}(a,b,f,P,z)$ be predicative formulas expressing the conditions of Predicative Formulas for Upper and Lower Darboux Sums, and the Maps and Sets of Darboux Sums over All Partitions (i) for $U$ and for $L$, with the parameters listed there; we use them with other set variables put for $a$, $b$, $f$, $P$ and $z$, by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i). By Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (iii), applied to the ordered field $\mathbb{R}$ (The Real Line: Standing Notation and Background for Calculus on Intervals (ii)) with its variables $t_{1},\dots,t_{6}$ renamed to the parameters $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$, there is a predicative formula $N(y,z)$, with free variables among $y$, $z$ and these parameters, which holds if and only if $y\in\mathbb{R}$ and $z=-y$. Let $\mu$ be the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii); pair memberships and the equation $p=(t,w)$ are the formulas of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii), and $u\le t$ and $u<v$ are memberships of ordered pairs in the parameters $\le$ and $<$ of $\mathbb{R}$. The letters $c$, $h$, $p$, $P$, $s$, $t$, $w$ and $y$ are set variables distinct from each other, from $g$, $u$, $v$, $z$ and from the parameters.

Proof of (i). The formula. Let

$$\mathrm{Lo}(u,v,h,z):\quad z\in\mathbb{R}\wedge\exists P\,\exists s\,\psi_{L}(u,v,h,P,s)\wedge\forall P\,\forall s\,(\psi_{L}(u,v,h,P,s)\Rightarrow s\le z)\wedge\forall c\,\bigl((c\in\mathbb{R}\wedge\forall P\,\forall s\,(\psi_{L}(u,v,h,P,s)\Rightarrow s\le c))\Rightarrow z\le c\bigr),$$

and let $\mathrm{Up}(u,v,h,z)$ be obtained from it by putting $\psi_{U}$ for $\psi_{L}$ and $z\le s$, $c\le s$ and $c\le z$ for $s\le z$, $s\le c$ and $z\le c$. Let

$$\rho(g,u,v,h):\quad\forall p\,\bigl(p\in h\Leftrightarrow(p\in g\wedge\exists t\,\exists w\,(p=(t,w)\wedge u\le t\wedge t\le v))\bigr),$$ $$J(g,u,v,z):\quad u<v\wedge\forall t\,\bigl((t\in\mathbb{R}\wedge u\le t\wedge t\le v)\Rightarrow t\in E\bigr)\wedge\exists h\,\bigl(\rho(g,u,v,h)\wedge\mathrm{Lo}(u,v,h,z)\wedge\mathrm{Up}(u,v,h,z)\bigr),$$

and

$$\Omega(g,u,v,z):\quad\mu(g,E,\mathbb{R})\wedge u\in E\wedge v\in E\wedge\Bigl((u=v\wedge z=0)\vee J(g,u,v,z)\vee\exists y\,\bigl(J(g,v,u,y)\wedge N(y,z)\bigr)\Bigr).$$

The free variables of $\Omega$ are among $g$, $u$, $v$, $z$ and the parameters.

Predicativity. $\psi_{U}$, $\psi_{L}$, $N$, $\mu$, the pair memberships and $p=(t,w)$ are predicative by the results cited above, and $\Omega$ is built from them, from memberships and from equations by connectives and by quantifiers over set variables only. So no quantifier of $\Omega$ is applied to a class variable, and $\Omega$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Meaning of Lo and Up. Let $u,v,h,z$ be sets. By Predicative Formulas for Upper and Lower Darboux Sums, and the Maps and Sets of Darboux Sums over All Partitions (i), $\psi_{L}(u,v,h,P,s)$ holds if and only if $u,v\in\mathbb{R}$, $u<v$, $h$ is a bounded map $h:[u,v]\to\mathbb{R}$, $P\in\Pi_{u,v}$ and $s=L(h,P)$. For $u<v$ in $\mathbb{R}$, $\{u,v\}=\{u\}\cup\{v\}$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iii) and Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (v), so it is a partition of $[u,v]$ by Partitions of a Closed Interval, the Set of Partitions, and Refinements (i), and $\Pi_{u,v}$ is nonempty by Partitions of a Closed Interval, the Set of Partitions, and Refinements (ii). Hence $\exists P\,\exists s\,\psi_{L}(u,v,h,P,s)$ holds if and only if $u,v\in\mathbb{R}$, $u<v$ and $h$ is a bounded map $h:[u,v]\to\mathbb{R}$. In that case the remaining conjuncts of $\mathrm{Lo}(u,v,h,z)$ say that $z\in\mathbb{R}$, $L(h,R)\le z$ for every partition $R$ of $[u,v]$, and $z\le c$ for every $c\in\mathbb{R}$ with $L(h,R)\le c$ for every partition $R$; by Bounds for Darboux Sums, Monotonicity under Refinement, the Supremum of the Lower Sums and the Infimum of the Upper Sums, and Concatenation of Partitions (iv), applied to $h$ on $[u,v]$, exactly one real number has these properties, and by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (iii) it is the lower integral of $h$ over $[u,v]$. So $\mathrm{Lo}(u,v,h,z)$ holds if and only if $u,v\in\mathbb{R}$, $u<v$, $h$ is a bounded map $h:[u,v]\to\mathbb{R}$ and $z$ is its lower integral over $[u,v]$; likewise $\mathrm{Up}(u,v,h,z)$ holds if and only if the same holds with the upper integral.

Meaning of J. Let $g:E\to\mathbb{R}$ be a map and let $u,v\in E$. If $u<v$ and $[u,v]\subseteq E$, then $\rho(g,u,v,h)$ holds exactly for $h=g|_{[u,v]}$: by The Restriction of a Function or Relation to a Class (i) the elements of $g|_{[u,v]}$ are the pairs $(t,w)\in g$ with $t\in[u,v]$, the first components of the pairs in $g$ lie in $E\subseteq\mathbb{R}$, and two sets with the same elements are equal (Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (ii)). Hence, by the meaning of $\mathrm{Lo}$ and $\mathrm{Up}$, $J(g,u,v,z)$ holds if and only if $u<v$, $[u,v]\subseteq E$, $g|_{[u,v]}:[u,v]\to\mathbb{R}$ is bounded and $z$ is both its lower and its upper integral, that is, by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (iv), The Riemann Integral on a Closed Interval via Lower and Upper Integrals (v) and The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi), if and only if $u<v$, $[u,v]\subseteq E$, $g$ is integrable on $[u,v]$ and $z=\int_{u}^{v}g$.

Meaning of $\Omega$. Let $g$, $u$, $v$ and $z$ be sets. If $g$ is not a map $g:E\to\mathbb{R}$, or $u\notin E$, or $v\notin E$, both $\Omega(g,u,v,z)$ and the condition fail, by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii). Otherwise $u,v\in\mathbb{R}$ and exactly one of $u=v$, $u<v$ and $v<u$ holds. If $u=v$, the second and third disjuncts fail, as they require $u<v$ or $v<u$; so $\Omega$ holds if and only if $z=0$, and $\int_{u}^{u}g$ is defined and equals $0$ by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vii). If $u<v$, the first and third disjuncts fail, and $\Omega$ holds if and only if $J(g,u,v,z)$, that is, if and only if $\int_{u}^{v}g$ is defined and $z=\int_{u}^{v}g$. If $v<u$, the first two disjuncts fail, and $\Omega$ holds if and only if $[v,u]\subseteq E$, $g$ is integrable on $[v,u]$ and $z=-\int_{v}^{u}g$, which is $\int_{u}^{v}g$ by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vii); that is, if and only if $\int_{u}^{v}g$ is defined and $z=\int_{u}^{v}g$. So $\Omega$ expresses the condition, as in Conditions Expressed by a Predicative Formula, and Guards (ii).

Proof of (ii). Indefinite integrals. Let $u\in K$. If $u=c$, $\int_{c}^{u}g$ is defined. If $c<u$, then $[c,u]\subseteq K$ by Intervals of the Real Line (i), and $g$ is integrable on $[c,u]$ by hypothesis; if $u<c$, then likewise $[u,c]\subseteq K$ and $g$ is integrable on $[u,c]$. So $\int_{c}^{u}g$ is defined, by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii); it is a real number, being $0$, a lower integral, which lies in $\mathbb{R}$ by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (iii), or the negative of one. Take $E=K$ and $g$ and $c$ as parameters, and let $\Omega$ be the formula above, with the parameter $c$ put for its set variable $u$ by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i) and the set variable $u$ then put for its variable $v$. By (i), for every $u\in K$ and every set $z$, $\Omega(g,c,u,z)$ holds if and only if $z=\int_{c}^{u}g$. Let

$$\Gamma=\{p\in K\times\mathbb{R}:\exists u\,\exists z\,(p=(u,z)\wedge\Omega(g,c,u,z))\},$$

a set by Sets and Maps: Ordinary Notation (iii) and Sets and Maps: Ordinary Notation (iv), its formula being predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). Its elements are the pairs $(u,\int_{c}^{u}g)$ with $u\in K$, so $\Gamma$ is a map $\Gamma:K\to\mathbb{R}$ with $\Gamma(u)=\int_{c}^{u}g$ for every $u\in K$, by Functions, Values of a Function, and Functions from One Class to Another (iii) and Functions, Values of a Function, and Functions from One Class to Another (ii); every map from $K$ to $\mathbb{R}$ with these values equals $\Gamma$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

Sequences of integrals. Let $\phi:\mathbb{N}\to\mathbb{R}^{[a,b]}$, $k\mapsto f_{k}$, be the given sequence (Sequences (i)). Take $E=[a,b]$, and $a$, $b$ and $\phi$ as parameters. For $k\in\mathbb{N}$, $f_{k}$ is a map $f_{k}:[a,b]\to\mathbb{R}$ by Sets and Maps: Ordinary Notation (v), and $f_{k}|_{[a,b]}=f_{k}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iii); as $f_{k}$ is bounded and integrable on $[a,b]$, it is integrable on $[a,b]$ in the sense of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi), with the same integral $\int_{a}^{b}f_{k}\in\mathbb{R}$. So, by (i) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), for every $k\in\mathbb{N}$ and every set $z$, $\exists h\,((k,h)\in\phi\wedge\Omega(h,a,b,z))$ holds if and only if $z=\int_{a}^{b}f_{k}$. As for $\Gamma$, the set

$$\Gamma'=\{p\in\mathbb{N}\times\mathbb{R}:\exists k\,\exists h\,\exists z\,(p=(k,z)\wedge(k,h)\in\phi\wedge\Omega(h,a,b,z))\},$$

with $k$ a further set variable, is a map $\Gamma':\mathbb{N}\to\mathbb{R}$ with $\Gamma'(k)=\int_{a}^{b}f_{k}$ for every $k\in\mathbb{N}$, that is, a sequence in $\mathbb{R}$ with these terms by Sequences (i), and it is the only one by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).