TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

Substitution for a continuous inner map with a Riemann-integrable extension of its interior derivative, without monotonicity or injectivity

Statement

Let $c < d$ , let $J = [p, q]$ with $p < q$ , and let $f : J \to R$ be continuous. Suppose $φ : [c, d] \to J$ is continuous on $[c, d]$ and differentiable on $(c, d)$ , and that the interior derivative has a Riemann-integrable extension $h : [c, d] \to R$ . Then $(f \circ φ) h$ is Riemann integrable and

$\int_{c}^{d} f (φ (t)) h (t) d t = \int_{φ (c)}^{φ (d)} f (x) d x .$

The limits on the right are oriented. No injectivity or monotonicity of $φ$ is required; the identity also covers $φ (c) > φ (d)$ and $φ (c) = φ (d)$ .

Facts & Assumptions

Given: The functions and intervals in the statement.

[L1]

A continuous integrand has an integral function differentiable at every point, with derivative equal to that integrand (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

[L2]

The chain rule gives $(H \circ φ)^{'} = (H^{'} \circ φ) φ^{'}$ on the interior (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[L3]

Continuous functions on a compact interval are Riemann integrable, and products of Riemann-integrable functions are Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, 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]

A continuous function with an interior derivative admitting an integrable extension satisfies Newton--Leibniz (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[L5]

Oriented integrals satisfy $\int_{u}^{u} f = 0$ and $\int_{v}^{u} f = - \int_{u}^{v} f$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

Proof

technique · reduction

1.1

Fix $r \in J$ and define $H (x) : = \int_{r}^{x} f$ with oriented limits. By [L1], $H$ is differentiable on $J$ and $H^{'} = f$ , including relative endpoint derivatives.

givenL1L5

1.2

The composite $f \circ φ$ is continuous and hence integrable; its product with the integrable $h$ is integrable by [L3].

givenL3

2.1

The composite $H \circ φ$ is continuous on $[c, d]$ , differentiable on $(c, d)$ , and [L2] gives $(H \circ φ)^{'} (t) = f (φ (t)) h (t)$ there.

givenstep 1.1L2

3.1

Applying [L4] to $H \circ φ$ gives $\int_{c}^{d} (f \circ φ) h = H (φ (d)) - H (φ (c))$ .

step 2.1step 1.2L4

4.1

The oriented definition in [L5] gives $H (v) - H (u) = \int_{u}^{v} f$ for every $u, v \in J$ , whether $u < v$ , $u = v$ , or $u > v$ . Taking $u = φ (c)$ and $v = φ (d)$ completes all three endpoint-order cases.

step 1.1L5algebra∎

Depends on

Used by

Riemannian length is invariant under orientation preserving piecewise c one reparametrization Theorem

Dependency tree · two levels

48 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. K. Hunter, An Introduction to Real Analysis, Theorem 12.12 (standard reference, not scraped)
J. Lebl, Basic Analysis I & II, Theorem 5.3.5 (standard reference, not scraped)