TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 100 results over 18 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

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)