Conventions of this page, and which sharpenings of the integral are taken up later in the reading order

This item is the ledger of the page: what "integrable" means here, what the orientation convention costs, what the page spends in choice, and which sharpenings of the integral belong to later pages rather than to this one. It establishes no theorem and serves only as a conventions and reading-order ledger.

"Integrable" on this page means Darboux integrable in the sense of The lower and upper Darboux integrals of a bounded $f$ on $[a,b]$ as ${\sup }_{P}L(f,P)$ and ${\inf }_{P}U(f,P)$, Darboux integrability as their equality, and the notation ${\int }_a^{b}f$, and ${\int }_a^{b}f$ is the common value of the lower and upper Darboux integrals. By The Darboux and Riemann definitions agree: a bounded $f$ on $[a,b]$ is Darboux integrable with integral $I$ if and only if for every real $\epsilon >0$ there is a real $\delta >0$ such that $\mathrm{\mid }S(f,P,\xi )-I\mathrm{\mid }<\epsilon$ for every tagged partition of mesh below $\delta$ that is the same class of functions with the same value as Riemann's own definition by tagged partitions of small mesh, so the two words are used interchangeably, as they are in the literature. No other integral is defined or used by a proof on this page or its companion.

The integral with oriented limits: ${\int }_a^{a}f:=0$ and ${\int }_b^{a}f:=-{\int }_a^{b}f$ extends the notation by ${\int }_u^{u}f:=0$ and ${\int }_u^{v}f:=-{\int }_v^{u}f$ for $u>v$. It is notation, not a new integral: the published definition is stated under the standing hypothesis $a<b$ and simply says nothing outside it.

Several statements on this page take their shape from that convention; three are worth naming, and no claim is made that they are the only ones.

• Additivity holds for every arrangement of three points. Claim 3 of For $a<c<b$: $f$ is integrable on $[a,b]$ if and only if it is integrable on $[a,c]$ and on $[c,b]$, and then ${\int }_a^{b}f={\int }_a^{c}f+{\int }_c^{b}f$; with the oriented form for arbitrary $a,b,c$ is ${\int }_u^{v}f+{\int }_v^{w}f={\int }_u^{w}f$ with no ordering assumed, and it is what makes The integral function $F(x):={\int }_a^{x}f$ of an integrable $f$'s identity $F(y)-F(x)={\int }_x^{y}f$ available in either order.
• Substitution keeps the limits in the order the map produces them. Substitution: if $\phi$ is differentiable on $[c,d]$ with ${\phi }^{\mathrm{\prime }}$ integrable and $f$ is continuous on an interval containing $\phi ([c,d])$, then ${\int }_{\phi (c)}^{\phi (d)}f={\int }_c^d(f\circ \phi ){\phi }^{\mathrm{\prime }}$ writes ${\int }_{\phi (c)}^{\phi (d)}f$ without assuming $\phi$ monotone or injective, and $\phi (d)<\phi (c)$ is allowed.
• One inequality is not orientation-invariant, and that is a trap. The estimate $\mid {\int }_u^{v}f\mid \le {\int }_u^v\mathrm{\mid }f\mathrm{\mid }$ of If $f,g$ are integrable on $[a,b]$ then so are $\mid f\mid$, $f^2$, $fg$, $\max (f,g)$ and $\min (f,g)$, and $\mid {\int }_a^{b}f\mid \le {\int }_a^b\mid f\mid$ is guaranteed only for $u\le v$; at $u>v$ its right-hand side is $\le 0$ while its left-hand side is $\ge 0$. The form valid for every pair is $\mid {\int }_u^{v}f\mid \le \mid {\int }_u^v\mathrm{\mid }f\mathrm{\mid }\mid$, and that item states both.

Nothing on this page introduces a new use of a choice principle. Every step that instantiates an existential statement does so finitely many times, which is ordinary first-order reasoning. The one place where a reader might expect a selection is The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G^{\mathrm{\prime }}=f$ and $f$ is integrable, then ${\int }_a^{b}f=G(b)-G(a)$: the classical proof picks a mean-value point ${\xi }_i$ in each subinterval of a partition and assembles a Riemann sum, and the proof given here does not, deriving instead the per-index inequality $m_i{\mathrm{\Delta }}_i\le G(t_{i+1})-G(t_i)\le M_i{\mathrm{\Delta }}_i$ and summing it. The same discipline is followed in Bonnet's second mean value theorem: for $f$ monotone and $g$ integrable on $[a,b]$ there is $\xi \in [a,b]$ with ${\int }_a^{b}fg=f(a){\int }_a^{\xi }g+f(b){\int }_{\xi }^{b}g$, where the approximating sums are built from the values of the integral function at the partition points and no tags are chosen.

The current Heine-Cantor in $\mathbb{R}$: a continuous real function on a compact subset of $\mathbb{R}$ is uniformly continuous proof uses a finite subcover and no countable choice. Its uses in A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion and If $f$ is integrable on $[a,b]$ with values in $[m,M]$ and $\phi$ is continuous on $[m,M]$, then $\phi \circ f$ is integrable add no choice cost. The forward half of Lebesgue's criterion for Riemann integrability: a bounded $f$ on $[a,b]$ is Riemann integrable if and only if its set of discontinuities has measure zero now uses the choice-free canonical rational-cover lemma, so its uses on this page add no choice cost. The choice ledger of the previous page, Choice ledger for the Riemann integral: the page results are proved in ZF, records the proofs' premises.

$\mathbb{N}$ contains $0$; a sequence is a function on $\mathbb{N}$; and a partition of $[a,b]$ is indexed from $i=0$, its first subinterval being $[t_0,t_1]$. Consequently The integral test: for $f\ge 0$ nonincreasing on $[0,\mathrm{\infty })$, ${\sum }_{k}f(k)$ converges if and only if the sequence $({\int }_0^{N}f{)}_N$ is bounded, with ${\int }_0^{N}f\le {\sum }_{k<N}f(k)\le f(0)+{\int }_0^{N}f$ is stated with both the sum and the integral beginning at $0$, and its bracket carries the term $f(0)$; the classical form beginning at $1$ is a statement about a tail, and this page does not silently substitute one for the other. A natural number multiplying or dividing a real always stands for its canonical natural.

Stated as reading order, and as no claim at all about what this library currently proves.

• Higher derivatives, and Taylor's theorem with the integral remainder. The integral remainder is an application of If $u,v$ are differentiable on $[a,b]$ with $u^{\mathrm{\prime }},v^{\mathrm{\prime }}$ integrable, then ${\int }_a^{b}u{v}^{\mathrm{\prime }}=u(b)v(b)-u(a)v(a)-{\int }_a^b{u}^{\mathrm{\prime }}v$ and needs derivatives of order $n$. The later Darboux/L'Hopital/Taylor page proves the Peano, Lagrange, Cauchy and Schlomilch-Roche forms but explicitly excludes the integral remainder. It is therefore absent from the current library, with no later published page assigned to it; this is a statement about the present reading order, not a theorem about Taylor remainders.
• Bounded variation and the Riemann–Stieltjes integral. The later bounded-variation page builds total variation, Jordan decomposition and the Riemann–Stieltjes integral. None is available at this point in the reading order, so nothing on the present page uses it.
• Improper integrals. ${\int }_0^{\mathrm{\infty }}f$ is not defined anywhere in this library at this point in the reading order, which is why The integral test: for $f\ge 0$ nonincreasing on $[0,\mathrm{\infty })$, ${\sum }_{k}f(k)$ converges if and only if the sequence $({\int }_0^{N}f{)}_N$ is bounded, with ${\int }_0^{N}f\le {\sum }_{k<N}f(k)\le f(0)+{\int }_0^{N}f$ concludes with the boundedness of the sequence $({\int }_0^{N}f{)}_N$ instead. Identifying the two is what that later page is for.
• Interchanging a limit with an integral. Pointwise convergence licenses nothing: the companion page's Continuous $f_n\to 0$ pointwise on $[0,1]$ with ${\int }_0^1{f}_n=1$ for every $n$ exhibits continuous $f_n\to 0$ pointwise on $[0,1]$ with ${\int }_0^1{f}_n=1$ for every $n$. What repairs it — uniform convergence, or a domination hypothesis — is not proved on this page and nothing here asserts any version of it.

Both are later results in the reading order. The sharp FTC is proved in Fundamental theorem of calculus for absolutely continuous functions and dominated convergence in Dominated convergence.

• Under Countable Choice and Dependent Choice, the sharp FTC identifies absolutely continuous real functions on $[a,b]$ with those satisfying $G^{\mathrm{\prime }}\in L^1$ almost everywhere and $G(x)=G(a)+{\int }_a^x{G}^{\mathrm{\prime }}$ for every $x$ in the interval. The two companion counterexamples, The sign function is Riemann integrable on $[-1,1]$ and has no primitive there and A function differentiable on $[0,1]$ whose derivative is unbounded, hence not Riemann integrable, show the limitations of the earlier primitive-based formulations.
• Dominated convergence licenses interchanging the pointwise almost-everywhere limit with the Lebesgue integral under an integrable domination hypothesis, providing the later sequel to the spike counterexample.