TheoremStatement: Literature-sourcedProof: AI-generatedprecheck 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 $ϕ : [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 R$ , $f is Riemann integrable ⟺ (f \circ ϕ) ∣ ϕ^{'} ∣ is Riemann integrable,$ and, when these conditions hold, $\int_{a}^{b} f (x) d x = \int_{c}^{d} f (ϕ (t)) ∣ ϕ^{'} (t) ∣ d t .$ Flat subintervals of $ϕ$ are allowed.

Facts & Assumptions

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

[L1]

On every subinterval, the mean value theorem writes $Δ ϕ = ϕ^{'} (η) Δ 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} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{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 $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ and $\min (f, g)$ , and $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ ).

[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 $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ ).

[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.1L1

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

2.1step 1.1L2L4

Compare the upper sum of $h$ on the transported partition with the upper sum of $(h \circ ϕ) ϕ^{'}$ on $P$ . [step 1.1, L2, L4] On each nonflat interval the two relevant suprema differ, after multiplication by $Δ t_{i}$ , by at most $M (U_{i} - u_{i}) Δ 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}) Δ t_{i} .$ Because $ϕ^{'}$ 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 ϕ) ϕ^{'}, \underline{\int_{a}^{b}} h = \underline{\int_{c}^{d}} (h \circ ϕ) ϕ^{'} .$ Thus one nonnegative function is integrable exactly when the other is, and their integrals then agree.

3.1step 2.1L3L5

For a general bounded $f$ , choose $M$ with $f + M \geq 0$ . Since $ϕ^{'}$ is integrable and $\int_{c}^{d} ϕ^{'} = ϕ (d) - ϕ (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$ .

4.1step 1.1step 2.1step 3.1∎

If $ϕ$ 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 $∣ ϕ^{'} ∣$ and the oriented-integral convention.

Depends on

Dependency tree · 2 levels

Sources

William F. Trench, Introduction to Real Analysis, Theorem 3.3.18