TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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.

If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable

Statement

Let $a < b$ and $m \leq M$ be reals, let $f : [a, b] \to R$ be integrable (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$ ) with

$m \leq f (x) \leq M for every x \in [a, b],$

and let $φ : [m, M] \to R$ be continuous on $[m, M]$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point). Then the composite $φ \circ f : [a, b] \to R$ is integrable on $[a, b]$ .

The order of the hypotheses is the whole content, and it does not reverse. What is assumed is continuous after integrable: the outer function is the continuous one. Weakening the outer function to a merely integrable $φ$ makes the statement false, and the witness is on the companion page. The remaining variant — $φ$ merely integrable with $f$ continuous — is neither proved nor refuted anywhere on this page, and the companion page's witness does not bear on it, its inner function being discontinuous at every rational. Nothing here asserts anything about that variant.

Facts & Assumptions

Given: Reals $a < b$ and $m \leq M$ , an integrable $f : [a, b] \to R$ with values in $[m, M]$ , a continuous $φ : [m, M] \to R$ , and a real $ε > 0$ . Write $h : = φ \circ f$ .

[L1]

Riemann's criterion: a bounded $u$ on $[a, b]$ is integrable if and only if for every real $η > 0$ there is a partition $P$ with $U (u, P) - L (u, P) < η$ (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ , 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$ ).

[L2]

For a partition $P = (n, t)$ of $[a, b]$ and bounded $u$ : $U (u, P) - L (u, P) = \sum_{i < n} (M_{i} (u) - m_{i} (u)) Δ_{i}$ with $Δ_{i} > 0$ and $\sum_{i < n} Δ_{i} = b - a$ , and $M_{i} (u) - m_{i} (u) = ω_{u} (I_{i}) = \sup {∣ u (x) - u (y) ∣ : x, y \in I_{i}}$ (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 oscillation $ω_{f} (S) = \sup {∣ f (x) - f (y) ∣ : x, y \in S}$ of $f$ on a set and the oscillation $ω_{f} (c) = \inf_{δ > 0} ω_{f} (A \cap N_{δ} (c))$ at a point, both taken in the extended reals, Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions, Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L3]

$[m, M]$ with $m \leq M$ and $[a, b]$ are closed bounded intervals, hence compact (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

A continuous real function on a compact subset of $R$ is bounded there (A continuous real function on a compact subset of $R$ is bounded, Lower bound, bounded below, bounded set).

[L5]

Heine-Cantor: a continuous real function on a compact $K \subseteq R$ is uniformly continuous on $K$ , so for every real $η > 0$ there is a real $δ_{0} > 0$ with $∣ φ (s) - φ (t) ∣ < η$ for all $s, t \in K$ with $∣ s - t ∣ < δ_{0}$ (Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous, Uniform continuity of $f : A \to R$ : one $δ$ serving every pair of points of $A$ ).

[L6]

Finite sums: additivity, scaling and monotonicity in the terms (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clauses 1, 2 and 4).

[L7]

Ordered-field arithmetic and the absolute value: multiplying an inequality by a nonnegative quantity and adding constants preserve it, the order is total and transitive, a positive real has a positive inverse, and $∣ u ∣ \leq c$ follows from $- c \leq u \leq c$ (Ordered field, Complete ordered field (least-upper-bound property), Basic properties of the absolute value). The nonstrict forms follow from the strict ones by adjoining the case of equality.

[L8]

For every real $η > 0$ there is a real $η^{'} > 0$ with $η^{'} < η$ , for instance $η^{'} = η \cdot 2^{- 1}$ ; and the Archimedean property in reciprocal form (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean).

Proof

technique · direct

1.1

$[m, M]$ is compact, so $φ$ is bounded there: fix a real $K \geq 0$ with $∣ φ (s) ∣ \leq K$ for every $s \in [m, M]$ . Hence $∣ h (x) ∣ \leq K$ for every $x \in [a, b]$ and $h$ is bounded.

givenL3L4choose

1.2

By [L5] applied on the compact $[m, M]$ with $η : = ε$ , fix a real $δ_{0} > 0$ with $∣ φ (s) - φ (t) ∣ < ε$ whenever $s, t \in [m, M]$ and $∣ s - t ∣ < δ_{0}$ ; then put $δ : = \min {δ_{0} \cdot 2^{- 1}, ε \cdot 2^{- 1}}$ , a positive real with $δ < δ_{0}$ and $δ < ε$ .

givenL3L5L7L8choose

2.1

So $∣ φ (s) - φ (t) ∣ \leq ε$ whenever $s, t \in [m, M]$ satisfy $∣ s - t ∣ \leq δ$ , since $δ < δ_{0}$ .

step 1.2L7

2.2

Since $δ > 0$ , so is $δ^{2}$ , and [L1] supplies a partition $P = (n, t)$ of $[a, b]$ with $U (f, P) - L (f, P) < δ^{2}$ .

step 1.2givenL1L7choose

3.1

Fix $i < n$ and write $Ω_{i} : = M_{i} (f) - m_{i} (f) \geq 0$ . If $Ω_{i} \leq δ$ then any $x, y \in I_{i}$ have $∣ f (x) - f (y) ∣ \leq Ω_{i} \leq δ$ with $f (x), f (y) \in [m, M]$ , so $∣ h (x) - h (y) ∣ \leq ε$ by step 2.1, whence $M_{i} (h) - m_{i} (h) \leq ε$ by [L2].

step 2.1step 2.2L2L7

3.2

If instead $Ω_{i} > δ$ then $Ω_{i} / δ > 1$ , while $M_{i} (h) - m_{i} (h) \leq 2 K$ always, by [L2] and step 1.1.

step 1.1step 2.2L2L7

4.1

In both cases $(M_{i} (h) - m_{i} (h)) Δ_{i} \leq ε Δ_{i} + (2 K / δ) Ω_{i} Δ_{i}$ : in the first case the second summand is nonnegative and the first alone dominates, and in the second case $(2 K / δ) Ω_{i} Δ_{i} \geq 2 K Δ_{i}$ dominates by itself.

step 3.1step 3.2L7

5.1

Summing over $i < n$ with [L6] and using $\sum_{i < n} Δ_{i} = b - a$ and [L2] gives $U (h, P) - L (h, P) \leq ε (b - a) + (2 K / δ) (U (f, P) - L (f, P))$ .

step 4.1L2L6L7

6.1

By step 2.2 the second summand is below $(2 K / δ) δ^{2} = 2 K δ$ , and $δ < ε$ by step 1.2, so $U (h, P) - L (h, P) < ε (b - a + 2 K)$ .

step 2.2step 5.1L7

7.1

Let a real $η > 0$ be given. Running steps 1.2 to 6.1 with $ε : = η / (b - a + 2 K + 1)$ , a positive real since $b - a + 2 K + 1 > 0$ , produces a partition $P$ with $U (h, P) - L (h, P) < η (b - a + 2 K) / (b - a + 2 K + 1) < η$ .

step 6.1L7L8

8.1

As $η > 0$ was arbitrary and $h$ is bounded by step 1.1, [L1] makes $h = φ \circ f$ integrable on $[a, b]$ .

step 1.1step 7.1L1∎

Remarks

Step 4.1 is what replaces the usual split of the index range. The classical proof separates the indices into a good set $G$ and a bad set $B$ and sums over each; the finite-sum toolkit used here is that of Laws of finite sums and finite products, stated for $\sum_{i < n}$ and carrying no clause that splits a range into a subset and its complement, so the split is carried instead by a single inequality valid at every index, whose two summands are exactly the two contributions. The bound obtained is the same one.
The hypothesis $f [[a, b]] \subseteq [m, M]$ is what makes $φ \circ f$ defined at all, and $m, M$ exist because an integrable $f$ is bounded (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}$ ). Taking $[m, M]$ to be any interval containing the range of $f$ is legitimate and changes nothing, since a continuous function on a larger compact interval restricts to a continuous one.
What the theorem does not say. It does not say that $φ \circ f$ is integrable when $φ$ is merely integrable, and it does not say that $\int_{a}^{b} φ \circ f$ can be computed from $\int_{a}^{b} f$ . The first is refuted on the companion page. For the second, take $φ (t) = t^{2}$ on $[0, 1]$ with $f$ the constant $1 / 2$ and with $g$ the indicator of $[0, 1 / 2]$ : both are integrable with integral $1 / 2$ , while $\int_{0}^{1} φ \circ f = 1 / 4$ and $\int_{0}^{1} φ \circ g = 1 / 2$ , so $\int_{a}^{b} φ \circ f$ is not a function of $\int_{a}^{b} f$ .
Forward reference, orientation only. The reversal refuted on the companion page is Integrable $φ$ and integrable $f$ with $φ \circ f$ not integrable: the order of the hypotheses in the composition theorem cannot be reversed ↗; nothing above depends on it.

Depends on

Used by

Dependency tree · two levels

60 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

Riemann integral (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 6 (standard reference, not scraped)
Springer article on compositions of Riemann-integrable functions (standard reference, not scraped)

If ff is integrable on [a,b][a,b] with values in [m,M][m,M] and φφ is continuous on [m,M][m,M], then φ∘fφ∘f is integrable