CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative

Statement

Let $a < b$ , let $φ$ be $C^{1}$ and injective on a neighborhood of $[a, b]$ , and suppose $φ^{'} (x) \neq 0$ there. If $f$ is continuous on an interval containing $φ ([a, b])$ , then $\int_{\min {φ (a), φ (b)}}^{\max {φ (a), φ (b)}} f (y) d y = \int_{a}^{b} f (φ (x)) ∣ φ^{'} (x) ∣ d x .$ Thus the absolute derivative is the correct factor for the unoriented image interval.

Facts & Assumptions

Given: The interval, injective $C^{1}$ map $φ$ , nonvanishing derivative, and continuous $f$ .

[L1]

A continuous injection on an interval is strictly increasing or strictly decreasing (A continuous injective function on an interval is strictly monotone).

[L2]

Oriented one-variable substitution gives $\int_{φ (a)}^{φ (b)} f = \int_{a}^{b} (f \circ φ) φ^{'}$ (Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ ).

[L3]

Compact-Jordan change of variables in dimension one uses the absolute Jacobian determinant (Change of variables for an injective $C^{1}$ map on a compact Jordan set).

Proof

technique · cases

1.1

Assume first that $φ$ is increasing. Every difference quotient using two points of $[a, b]$ is nonnegative, so an inward sequence at either endpoint and a two-sided sequence in the interior show that the derivative is nonnegative; nonvanishing makes it positive throughout. Thus [L2] is exactly the displayed formula.

L1L2givenassume-case increasing

1.2

Assume instead that $φ$ is decreasing. The same inward difference-quotient argument makes $φ^{'} \leq 0$ on $[a, b]$ , so nonvanishing makes $φ^{'} < 0$ throughout. This reverses both the oriented endpoints and the derivative sign in [L2], and consequently gives $\int_{φ (b)}^{φ (a)} f = \int_{a}^{b} (f \circ φ) ∣ φ^{'} ∣ .$

L1L2givenassume-case decreasing

2.1

The alternatives are exhaustive by [L1], and [L3] identifies $∣ φ^{'} ∣$ with the one-dimensional absolute Jacobian factor.

L1L3cases-exhaustive: increasing or decreasing∎

Depends on

Used by

Omitting the absolute value from the Jacobian gives negative length under the reflection x↦1-x Counterexample

Dependency tree · two levels

36 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. Lebl, Basic Analysis II, Theorem 10.7.2 and one-variable substitution (standard reference, not scraped)