Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-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.

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

Statement

Let a<ba<b, let φ\varphi be C1C^1 and injective on a neighborhood of [a,b][a,b], and suppose φ′(x)≠0\varphi'(x)\ne0 there. If ff is continuous on an interval containing φ([a,b])\varphi([a,b]), then ∫min⁡{φ(a),φ(b)}max⁡{φ(a),φ(b)}f(y) dy=∫abf(φ(x))∣φ′(x)∣ dx.\int_{\min\{\varphi(a),\varphi(b)\}}^{\max\{\varphi(a),\varphi(b)\}}f(y)\,dy=\int_a^b f(\varphi(x))|\varphi'(x)|\,dx. Thus the absolute derivative is the correct factor for the unoriented image interval.

Facts & Assumptions

Given: The interval, injective C1C^1 map φ\varphi, nonvanishing derivative, and continuous ff.

[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 ∫φ(a)φ(b)f=∫ab(f∘φ)φ′\int_{\varphi(a)}^{\varphi(b)}f=\int_a^b(f\circ\varphi)\varphi' (Substitution: if φ\varphi is differentiable on [c,d][c,d] with φ′\varphi' integrable and ff is continuous on an interval containing φ([c,d])\varphi([c,d]), then ∫φ(c)φ(d)f=∫cd(f∘φ) φ′\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi').

[L3]

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

Proof

technique · cases
1.1

Assume first that φ\varphi is increasing. Every difference quotient using two points of [a,b][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 φ\varphi is decreasing. The same inward difference-quotient argument makes φ′≤0\varphi'\le0 on [a,b][a,b], so nonvanishing makes φ′<0\varphi'<0 throughout. This reverses both the oriented endpoints and the derivative sign in [L2], and consequently gives ∫φ(b)φ(a)f=∫ab(f∘φ)∣φ′∣.\int_{\varphi(b)}^{\varphi(a)}f=\int_a^b(f\circ\varphi)|\varphi'|.

L1L2givenassume-case decreasing
2.1

The alternatives are exhaustive by [L1], and [L3] identifies ∣φ′∣|\varphi'| with the one-dimensional absolute Jacobian factor.

L1L3cases-exhaustive: increasing or decreasing∎

Depends on

Used by

Dependency tree · next 3 levels

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