TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Monotone change of variable for Riemann-integrable functions

Statement

Let $\phi:[c,d]\to[a,b]$ be a monotone surjection, differentiable on $[c,d]$ in the one-sided endpoint sense, with Riemann-integrable derivative. For every bounded $f:[a,b]\to\mathbb R$ , $f\text{ is Riemann integrable}\quad\Longleftrightarrow\quad(f\circ\phi)|\phi'|\text{ is Riemann integrable},$ and, when these conditions hold, $\int_a^b f(x)\,dx=\int_c^d f(\phi(t))|\phi'(t)|\,dt.$ Flat subintervals of $\phi$ are allowed.

Facts & Assumptions

Given: The monotone differentiable surjection $\phi$ with integrable derivative and a bounded $f$ .

[L1]

On every subinterval, the mean value theorem writes $\Delta\phi=\phi'(\eta)\Delta t$ (The mean value theorem, as the case $g(x) = x$ of Cauchy's: for $f$ continuous on $[a,b]$ with $a < b$ and differentiable on $(a,b)$ there is $c \in (a,b)$ with $f(b) - f(a) = f'(c)(b-a)$ ).

[L2]

Darboux integrability is equivalent to arbitrarily small upper-minus-lower sums (For bounded $f$ on $[a,b]$ and a partition $P$ : the infimum $m_i$ and supremum $M_i$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L(f,P) = \sum_i m_i \Delta_i$ and $U(f,P) = \sum_i M_i \Delta_i$ , 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$ ).

[L3]

Products, absolute values, and positive and negative parts of Riemann-integrable functions are integrable (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$ ).

[L4]

Darboux integrals agree with tagged Riemann-sum limits (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$ ).

[L5]

The integral of an integrable derivative is the endpoint difference (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)$ ).

Proof

technique · direct

1.1

Assume first that $\phi$ is nondecreasing, and let $0\le h\le M$ . [L1] For a partition $P=\{t_i\}$ of $[c,d]$ , transport its points through $\phi$ and delete repeated image points. If $U_i,u_i$ are the supremum and infimum of $\phi'$ on $[t_{i-1},t_i]$ , the mean value theorem gives $u_i\Delta t_i\le \phi(t_i)-\phi(t_{i-1})\le U_i\Delta t_i.$ On a flat interval the image increment is zero and $\phi'=0$ in its interior, so its contribution may be discarded.

2.1

Compare the upper sum of $h$ on the transported partition with the upper sum of $(h\circ\phi)\phi'$ on $P$ . [step 1.1, L2, L4] On each nonflat interval the two relevant suprema differ, after multiplication by $\Delta t_i$ , by at most $M(U_i-u_i)\Delta t_i$ ; the identical estimate holds for lower sums. Hence each pair of corresponding sums differs by at most $M\sum_i(U_i-u_i)\Delta t_i.$ Because $\phi'$ is integrable, refinements can make this error arbitrarily small. Taking upper and lower integrals therefore gives $\overline{\int_a^b}h=\overline{\int_c^d}(h\circ\phi)\phi',\qquad \underline{\int_a^b}h=\underline{\int_c^d}(h\circ\phi)\phi'.$ Thus one nonnegative function is integrable exactly when the other is, and their integrals then agree.

3.1

For a general bounded $f$ , choose $M$ with $f+M\ge0$ . Since $\phi'$ is integrable and $\int_c^d\phi'=\phi(d)-\phi(c)=b-a$ , applying step 2.1 to $f+M$ and subtracting the constant term proves both the integrability equivalence and the integral identity for $f$ .

step 2.1L3L5

4.1

If $\phi$ is nonincreasing, reverse the source orientation and apply steps 1.1–3.1 to the resulting nondecreasing parametrization. The sign reversal is exactly removed by $|\phi'|$ and the oriented-integral convention.

step 1.1step 2.1step 3.1∎

Depends on

Used by

Change of variable in an improper integral Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 113 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

William F. Trench, Introduction to Real Analysis, Theorem 3.3.18 (standard reference, not scraped)