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 $\varepsilon > 0$ there is a real $\delta > 0$ such that $|S(f,P,\xi) - I| < \varepsilon$ 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 $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$, then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$ writes $\int_{\varphi(c)}^{\varphi(d)} f$ without assuming $\varphi$ monotone or injective, and $\varphi(d) < \varphi(c)$ is allowed.
• One inequality is not orientation-invariant, and that is a trap. The estimate $\bigl|\int_u^v f\bigr| \le \int_u^v |f|$ of If $f,g$ are integrable on $[a,b]$ then so are $\lvert f\rvert$, $f^{2}$, $fg$, $\max(f,g)$ and $\min(f,g)$, and $\bigl\lvert\int_a^b f\bigr\rvert \le \int_a^b\lvert f\rvert$ 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 $\bigl|\int_u^v f\bigr| \le \bigl|\int_u^v |f|\,\bigr|$, 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' = 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\Delta_i \le G(t_{i+1})-G(t_i) \le M_i\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.

Choice does enter through published items that name their own cost, and those costs are inherited unchanged, not added to: Heine-Cantor in $\mathbb{R}$: a continuous real function on a compact subset of $\mathbb{R}$ is uniformly continuous, proved $\mathbb{R}$-natively from sequential compactness spends countable choice once, and every item here that rests on A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion or on If $f$ is integrable on $[a,b]$ with values in $[m,M]$ and $\varphi$ is continuous on $[m,M]$, then $\varphi \circ f$ is integrable inherits that single use. 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 spends countable choice once in the half that goes from integrability to the discontinuity set being null, and the companion page uses that half; that use too is inherited and not new. The choice ledger of the previous page, What this page costs in choice: Riemann's criterion, the Darboux-Riemann equivalence and integrability of a monotone function are theorems of ZF; integrability of a continuous function inherits the single use of countable choice inside Heine-Cantor; and only the forward half of the Lebesgue criterion spends countable choice, once, at the countable union of null sets, records the costs of the published items themselves.

$\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,\infty)$, $\sum_k f(k)$ converges if and only if the sequence $\bigl(\int_0^N f\bigr)_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',v'$ integrable, then $\int_a^b u v' = u(b)v(b)-u(a)v(a) - \int_a^b u'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^{\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,\infty)$, $\sum_k f(k)$ converges if and only if the sequence $\bigl(\int_0^N f\bigr)_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 $\bigl(\int_0^N f\bigr)_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 recorded elsewhere as results the library does not establish, and they are mentioned here for orientation only; nothing on this page or its companion rests on either.

• The sharp fundamental theorem of calculus (absolute continuity) ‡ — the sharp form of the fundamental theorem: the absolutely continuous functions are exactly those for which $G'$ exists almost everywhere, $G'\in L^1$, and $G(x)=G(a)+\int_a^x G'$ for every $x\in[a,b]$. The two counterexamples on the companion page, 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 ↗, are precisely the two ways the naive form fails, and that sharp form is the answer.
• Dominated convergence theorem ‡ — the theorem that licenses interchanging a limit with an integral under a domination hypothesis, and the natural sequel to the spike counterexample above.