Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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 ff is integrable on [a,b][a,b] with values in [m,M][m,M] and φ\varphi is continuous on [m,M][m,M], then φf\varphi \circ f is integrable

Statement

Let a<ba < b and mMm \le M be reals, let f:[a,b]Rf : [a,b] \to \mathbb{R} be integrable (The lower and upper Darboux integrals of a bounded ff on [a,b][a,b] as supPL(f,P)\sup_P L(f,P) and infPU(f,P)\inf_P U(f,P), Darboux integrability as their equality, and the notation abf\int_a^b f) with

m    f(x)    Mfor every x[a,b],m \;\le\; f(x) \;\le\; M \qquad \text{for every } x \in [a,b],

and let φ:[m,M]R\varphi : [m,M] \to \mathbb{R} be continuous on [m,M][m,M] (Continuity of f:ARf : A \to \mathbb{R} at a point of AA and on AA: the ε\varepsilon-δ\delta condition, its agreement with limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) at a limit point, and continuity at an isolated point). Then the composite φf:[a,b]R\varphi \circ f : [a,b] \to \mathbb{R} is integrable on [a,b][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 φ\varphi makes the statement false, and the witness is on the companion page. The remaining variant — φ\varphi merely integrable with ff 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<ba < b and mMm \le M, an integrable f:[a,b]Rf : [a,b] \to \mathbb{R} with values in [m,M][m,M], a continuous φ:[m,M]R\varphi : [m,M] \to \mathbb{R}, and a real ε>0\varepsilon > 0. Write h:=φfh := \varphi \circ f.

[L2]

For a partition P=(n,t)P = (n,t) of [a,b][a,b] and bounded uu: U(u,P)L(u,P)=i<n(Mi(u)mi(u))ΔiU(u,P) - L(u,P) = \sum_{i<n}\bigl(M_i(u) - m_i(u)\bigr)\Delta_i with Δi>0\Delta_i > 0 and i<nΔi=ba\sum_{i<n}\Delta_i = b - a, and Mi(u)mi(u)=ωu(Ii)=sup{u(x)u(y):x,yIi}M_i(u) - m_i(u) = \omega_u(I_i) = \sup\{\,|u(x)-u(y)| : x,y \in I_i\,\} (For bounded ff on [a,b][a,b] and a partition PP: the infimum mim_i and supremum MiM_i of ff on the ii-th subinterval, and the lower and upper Darboux sums L(f,P)=imiΔiL(f,P) = \sum_i m_i \Delta_i and U(f,P)=iMiΔiU(f,P) = \sum_i M_i \Delta_i, The oscillation ωf(S)=sup{f(x)f(y):x,yS}\omega_f(S) = \sup\{\,|f(x) - f(y)| : x, y \in S\,\} of ff on a set and the oscillation ωf(c)=infδ>0ωf(ANδ(c))\omega_f(c) = \inf_{\delta > 0} \omega_f(A \cap N_\delta(c)) at a point, both taken in the extended reals, Partition of [a,b][a,b] as a finite strictly increasing list a=t0<t1<<tn=ba = 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).

[L4]

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

[L5]

Heine-Cantor: a continuous real function on a compact KRK \subseteq \mathbb{R} is uniformly continuous on KK, so for every real η>0\eta > 0 there is a real δ0>0\delta_0 > 0 with φ(s)φ(t)<η|\varphi(s)-\varphi(t)| < \eta for all s,tKs,t \in K with st<δ0|s-t| < \delta_0 (Heine-Cantor in R\mathbb{R}: a continuous real function on a compact subset of R\mathbb{R} is uniformly continuous, proved R\mathbb{R}-natively from sequential compactness, Uniform continuity of f:ARf : A \to \mathbb{R}: one δ\delta serving every pair of points of AA).

[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 uc|u| \le c follows from cuc-c \le u \le 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\eta > 0 there is a real η>0\eta' > 0 with η<η\eta' < \eta, for instance η=η21\eta' = \eta \cdot 2^{-1}; and the Archimedean property in reciprocal form (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean).

Proof

technique · direct
1.1

[m,M][m,M] is compact, so φ\varphi is bounded there: fix a real K0K \ge 0 with φ(s)K|\varphi(s)| \le K for every s[m,M]s \in [m,M]. Hence h(x)K|h(x)| \le K for every x[a,b]x \in [a,b] and hh is bounded.

givenL3L4choose
1.2

By [L5] applied on the compact [m,M][m,M] with η:=ε\eta := \varepsilon, fix a real δ0>0\delta_0 > 0 with φ(s)φ(t)<ε|\varphi(s)-\varphi(t)| < \varepsilon whenever s,t[m,M]s,t \in [m,M] and st<δ0|s-t| < \delta_0; then put δ:=min{δ021, ε21}\delta := \min\{\delta_0 \cdot 2^{-1},\ \varepsilon \cdot 2^{-1}\}, a positive real with δ<δ0\delta < \delta_0 and δ<ε\delta < \varepsilon.

givenL3L5L7L8choose
2.1

So φ(s)φ(t)ε|\varphi(s)-\varphi(t)| \le \varepsilon whenever s,t[m,M]s,t \in [m,M] satisfy stδ|s-t| \le \delta, since δ<δ0\delta < \delta_0.

step 1.2L7
2.2

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

step 1.2givenL1L7choose
3.1

Fix i<ni < n and write Ωi:=Mi(f)mi(f)0\Omega_i := M_i(f) - m_i(f) \ge 0. If Ωiδ\Omega_i \le \delta then any x,yIix,y \in I_i have f(x)f(y)Ωiδ|f(x)-f(y)| \le \Omega_i \le \delta with f(x),f(y)[m,M]f(x),f(y) \in [m,M], so h(x)h(y)ε|h(x)-h(y)| \le \varepsilon by step 2.1, whence Mi(h)mi(h)εM_i(h) - m_i(h) \le \varepsilon by [L2].

step 2.1step 2.2L2L7
3.2

If instead Ωi>δ\Omega_i > \delta then Ωi/δ>1\Omega_i/\delta > 1, while Mi(h)mi(h)2KM_i(h) - m_i(h) \le 2K always, by [L2] and step 1.1.

step 1.1step 2.2L2L7
4.1

In both cases (Mi(h)mi(h))ΔiεΔi+(2K/δ)ΩiΔi\bigl(M_i(h)-m_i(h)\bigr)\Delta_i \le \varepsilon\,\Delta_i + \bigl(2K/\delta\bigr)\Omega_i\Delta_i: in the first case the second summand is nonnegative and the first alone dominates, and in the second case (2K/δ)ΩiΔi2KΔi(2K/\delta)\Omega_i\Delta_i \ge 2K\Delta_i dominates by itself.

step 3.1step 3.2L7
5.1

Summing over i<ni < n with [L6] and using i<nΔi=ba\sum_{i<n}\Delta_i = b-a and [L2] gives U(h,P)L(h,P)ε(ba)+(2K/δ)(U(f,P)L(f,P))U(h,P)-L(h,P) \le \varepsilon(b-a) + (2K/\delta)\bigl(U(f,P)-L(f,P)\bigr).

step 4.1L2L6L7
6.1

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

step 2.2step 5.1L7
7.1

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

step 6.1L7L8
8.1

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

step 1.1step 7.1L1

Remarks

Depends on

Used by

Dependency tree · next 3 levels

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