Alphabeta Math
Session-authored (Fable 5 assisted)
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.

6 results · all verified · 2 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Lebesgue and Riemann Integrals Compared

1 · Prerequisites

2 · Summary

This page is the seam between the elementary Riemann theory and the Lebesgue integral. The main comparison theorem is proved by Darboux envelopes rather than by quoting the already-published null-discontinuity criterion A bounded function on a closed bounded interval, or on a closed nondegenerate rectangle, is Riemann integrable exactly when its discontinuity set has Lebesgue measure zero: the point of the route here is to make the completeness of Lebesgue measure visible.

The page also records the comparison corollaries that belong exactly at that seam. Arzela's bounded convergence theorem becomes a short consequence of Lebesgue bounded convergence, nonnegative improper half-line integrals pass to Lebesgue integrals by monotone convergence, and the continuous Riemann-Stieltjes integral is identified with integration against the corresponding Lebesgue-Stieltjes measure. The published Jordan-content and Lebesgue-criterion agreement theorems remain earlier inputs and are cited in summary rather than duplicated here.

3 · Logical flowchart

4 · Definitions, theorems and proofs

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-28Open item page →

A bounded Riemann integrable function admits Borel Darboux envelopes with the same Lebesgue integral

Statement

Assume the Axiom of Countable Choice. Let a<b, let f:[a,b]R be bounded and Riemann integrable, and write I:=abf(x)dx for its Riemann integral. Then there exist bounded Borel functions φ,ψ:[a,b]R such that

φ(x)f(x)ψ(x)(x[a,b]),

[a,b]φdλ1=I=[a,b]ψdλ1.

In particular, [a,b](ψφ)dλ1=0.

Facts & Assumptions

Given: The Axiom of Countable Choice, reals a<b, a bounded Riemann integrable function f:[a,b]R with Riemann integral I, and a real B>0 with f(x)B for every x[a,b].

[L1]

Riemann's criterion says that for every real ε>0 there is a partition P of [a,b] with U(f,P)L(f,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)<ε)

[L3]

The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra. (The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra)

[L4]

Pointwise infima of measurable functions are measurable, and the pointwise limit of an increasing sequence of measurable functions is measurable. (Closure properties of measurable functions used by the integral)

[L6]

The nonnegative integral agrees with the simple integral on nonnegative simple functions, and the simple integral of jcjχEj is jcjμ(Ej). (The nonnegative integral agrees with the simple integral on simple functions, The integral of a nonnegative simple function)

[L7]

Monotone convergence holds for nonnegative measurable functions. (Monotone convergence for the integral)

[L9]

A measurable real function is integrable exactly when the integral of its absolute value is finite, and the Lebesgue integral is linear on L1. (Integrable real and complex functions, and their integrals, The Lebesgue integral is linear on L1(μ))

[L10]

For every real η>0 there is a natural number N1 with 1/N<η. (For every ε>0 in a complete ordered field there is a natural n1 with 1/n<ε)

Proof

technique · direct
1.1

By [L1], choose recursively a refining sequence of partitions P1P2 of [a,b] such that U(f,Pn)L(f,Pn)<1/n for every n1: choose P1 for ε=1, and once Pn is chosen, let Rn+1 satisfy U(f,Rn+1)L(f,Rn+1)<1/(n+1) and put Pn+1:=PnRn+1; then [L2] preserves the inequality under refinement. For each n, write Pn={a=t0(n)<<tmn(n)=b} and let mn,i and Mn,i be the infimum and supremum of f on [ti(n),ti+1(n)]. Define n:=mn,mn1χ{b}+i<mnmn,iχ[ti(n),ti+1(n)), un:=Mn,mn1χ{b}+i<mnMn,iχ[ti(n),ti+1(n)). Each partition piece is a Borel subset of [a,b] by [L3], so n and un are bounded Borel functions on [a,b]. Also Bnn+1fun+1unB pointwise, while [L11] gives L(f,Pn)IU(f,Pn),U(f,Pn)L(f,Pn)<1/n.

L1L2L3chooseconstruct
2.1

Put φ:=supnn and ψ:=infnun. Since nφ, the last clause of [L4] makes φ Borel measurable; since un are measurable, the infimum clause of [L4] makes ψ Borel measurable. Step 1.1 gives BφfψB. Now B+n is a nonnegative simple function, so [L6] and [L8] give [a,b](B+n)dλ1=B(ba)+L(f,Pn). Because B+nB+φ, [L7] yields [a,b](B+φ)dλ1=limn(B(ba)+L(f,Pn))=B(ba)+I, the limit being the squeeze from step 1.1. Since (B+φ)Bχ[a,b]=φBχ[a,b], the constant function Bχ[a,b] is integrable by [L6] and [L8], so step 1.1 and [L5], [L9] show that φL1(λ1) and [a,b]φdλ1=I.

step 1.1L4L5L6L7L8L9
3.1

For each n the function unn is nonnegative simple, and step 1.1 with [L6] and [L8] gives [a,b](unn)dλ1=U(f,Pn)L(f,Pn)<1/n. Because φfψ and nφψun, one has 0ψφunn for every n. So [L5] yields 0[a,b](ψφ)dλ1<1/n(n1). If that integral were positive, [L10] would give n with 1/n<[a,b](ψφ)dλ1, contradicting the displayed inequality. Therefore [a,b](ψφ)dλ1=0. The same bound ψφ2Bχ[a,b] shows ψφL1(λ1).

step 1.1step 2.1L5L6L8L9L10
4.1

Since ψ=φ+(ψφ) and both summands are integrable, [L9] and step 3.1 give [a,b]ψdλ1=[a,b]φdλ1+[a,b](ψφ)dλ1=I+0=I. Together with steps 2.1 and 3.1, this proves the existence of bounded Borel envelopes φfψ with the same Lebesgue integral I.

step 2.1step 3.1L9
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-28Open item page →

A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral

Statement

Assume the Axiom of Countable Choice. Let a<b and let f:[a,b]R be bounded and Riemann integrable. Then f is Lebesgue measurable on [a,b] and is integrable there, and its Lebesgue integral equals its Riemann integral: [a,b]fdλ1=abf(x)dx.

This is the point at which the completeness of Lebesgue measure is used essentially: the proof obtains a Borel function equal to f almost everywhere, and measurability of f itself is then a completeness statement.

Facts & Assumptions

Given: The Axiom of Countable Choice, reals a<b, a bounded Riemann integrable function f:[a,b]R, its Riemann integral I:=abf(x)dx, and a real B>0 with f(x)B on [a,b].

[L1]

The envelope lemma produces bounded Borel functions φ,ψ:[a,b]R with φfψ and [a,b]φdλ1=I=[a,b]ψdλ1. (A bounded Riemann integrable function admits Borel Darboux envelopes with the same Lebesgue integral)

[L2]

A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere. (A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere)

[L3]

On a complete measure space, a function equal almost everywhere to a measurable function is measurable. (On a complete measure space, equality almost everywhere preserves measurability)

[L5]

Two integrable functions that agree almost everywhere have the same integral over every measurable set. (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree)

[L6]

If a real measurable function is bounded in absolute value by a nonnegative integrable function, then its absolute value has finite integral; a measurable real function is integrable exactly when the integral of its absolute value is finite. (Closure properties of measurable functions used by the integral, Monotonicity and nonnegative homogeneity of the nonnegative integral, The nonnegative integral agrees with the simple integral on simple functions, The integral of a nonnegative simple function, Integrable real and complex functions, and their integrals)

Proof

technique · direct
1.1

By [L1], choose bounded Borel functions φ,ψ on [a,b] with [L1, L2] φfψ and both integrals equal to I. Then 0ψφ and [a,b](ψφ)dλ1=0. So [L2] gives ψ=φ almost everywhere. Since φfψ, the same null set yields f=φ almost everywhere.

2.1

By [L4], the measure space (R,L(R),λ1) is [step 1.1, L3, L4] complete. The function φ is measurable because it is Borel, so [L3] applied to step 1.1 shows that f is Lebesgue measurable.

3.1

The constant function Bχ[a,b] is a nonnegative simple measurable [step 2.1, L1, L6, L7] function, and [L6] together with [L7] gives [a,b]Bχ[a,b]dλ1=B(ba)<+. Since step 2.1 makes f measurable and fBχ[a,b], [L6] yields [a,b]fdλ1<+. Hence f is Lebesgue integrable on [a,b]. The same estimate applies to φ, because [L1] gives φB.

4.1

Steps 1.1 and 3.1 show that f and φ are integrable and agree [step 1.1, step 3.1, L1, L5] almost everywhere. Taking the measurable set A=[a,b] in [L5] gives [a,b]fdλ1=[a,b]φdλ1. By [L1], the right-hand side is I=abf(x)dx. So the Lebesgue and Riemann integrals of f agree. ∎

CorollaryStatement: AI-generatedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

A Riemann integrable function on a closed bounded interval is almost everywhere equal to a Borel function

Statement

Assume the Axiom of Countable Choice. Let a<b and let f:[a,b]R be Riemann integrable. Then there is a Borel function g:[a,b]R such that f=g almost everywhere on [a,b].

Facts & Assumptions

Given: The Axiom of Countable Choice, reals a<b, and a Riemann integrable function f:[a,b]R.

[L1]

The envelope lemma gives bounded Borel functions φ,ψ:[a,b]R with φfψ and [a,b](ψφ)dλ1=0. (A bounded Riemann integrable function admits Borel Darboux envelopes with the same Lebesgue integral)

[L2]

A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere. (A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere)

Proof

technique · direct
1.1

By [L1], choose bounded Borel functions φ,ψ with [L1, L2] φfψ and [a,b](ψφ)dλ1=0. Since ψφ0, [L2] gives ψ=φ almost everywhere on [a,b].

2.1

On the same full-measure set one has [step 1.1, L1] φfψ=φ, so f=φ almost everywhere. Taking g:=φ proves the claim, and g is Borel by step 1.1. ∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Arzela's bounded convergence theorem for Riemann integrals

Statement

Assume the Axiom of Countable Choice. Let a<b, let fn:[a,b]R be Riemann integrable for every n, and let f:[a,b]R be Riemann integrable. Suppose that fn(x)f(x) for every x[a,b] and that there is a real M0 with fn(x)M for all n and all x[a,b]. Then abfn(x)dxabf(x)dx.

Facts & Assumptions

Given: The Axiom of Countable Choice, reals a<b, Riemann integrable functions f,fn:[a,b]R with fn(x)f(x) for every x[a,b], and a real M0 with fn(x)M for all n and x.

[L1]

A bounded Riemann integrable function on [a,b] is Lebesgue measurable, Lebesgue integrable, and has the same Lebesgue and Riemann integrals. (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral)

[L2]

On a finite measure space, almost-everywhere pointwise convergence of a uniformly bounded measurable sequence implies convergence of the integrals. (Bounded convergence on a finite measure space)

Proof

technique · direct
1.1

By [L1], each fn and f is Lebesgue measurable and integrable on [a,b], and [a,b]fndλ1=abfn(x)dx,[a,b]fdλ1=abf(x)dx. Also [L3] makes ([a,b],L([a,b]),λ1) a finite measure space.

L1L3
2.1

The convergence hypothesis is pointwise, hence almost everywhere, and the uniform bound fnM holds everywhere. So [L2] applies on [a,b] and gives [a,b]fndλ1[a,b]fdλ1. Translating the two sides with step 1.1 yields the stated convergence of the Riemann integrals.

step 1.1L2
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-28Open item page →

A nonnegative improper Riemann integral on a half-line agrees with the Lebesgue integral

Statement

Assume the Axiom of Countable Choice. Let aR and let f:[a,)[0,) be Riemann integrable on every compact interval [a,R] with R>a. If the improper Riemann integral af(x)dx converges in the sense of Improper integrals over unbounded intervals, then f is Lebesgue integrable on [a,) and [a,)fdλ1=af(x)dx.

Facts & Assumptions

Given: The Axiom of Countable Choice, a real a, a nonnegative function f:[a,)[0,) that is Riemann integrable on every [a,R] with R>a, and a finite improper Riemann integral L:=af(x)dx.

[L1]

On every compact interval, a bounded Riemann integrable function is Lebesgue integrable there with the same value. (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral)

[L2]

Monotone convergence holds for nonnegative measurable functions. (Monotone convergence for the integral)

[L3]

The improper integral over [a,) is the limit of the truncated Riemann integrals as the right endpoint tends to +. (Improper integrals over unbounded intervals)

Proof

technique · direct
1.1

For each natural number n1, define fn:=fχ[a,a+n]. Then 0fnfn+1 and fn(x)f(x) for every xa. By [L1] applied on [a,a+n], [a,)fndλ1=[a,a+n]fdλ1=aa+nf(x)dx.

L1construct
2.1

Since fnf, [L2] gives [a,)fdλ1=limn[a,)fndλ1=limnaa+nf(x)dx. Because a+n+, [L3] identifies the last limit with the given improper integral L. Hence [a,)fdλ1=L, and in particular the Lebesgue integral is finite, so f is integrable on the half-line.

step 1.1L2L3
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-28Open item page →

For a continuous integrand, the Riemann-Stieltjes and Lebesgue-Stieltjes integrals agree

Statement

Assume the Axiom of Countable Choice. Let a<b, let g:[a,b]R be continuous, let F:RR be nondecreasing and right-continuous, and let μF be the Lebesgue-Stieltjes measure attached to F. Then g is μF-integrable on (a,b] and abgdF=(a,b]gdμF.

Facts & Assumptions

Given: The Axiom of Countable Choice, reals a<b, a continuous function g:[a,b]R, a nondecreasing right-continuous function F:RR, its Lebesgue-Stieltjes measure μF, the Riemann-Stieltjes integral I:=abgdF, and a real B>0 with g(x)B on [a,b].

[L1]

A continuous integrand is Riemann-Stieltjes integrable against every bounded-variation integrator; since a nondecreasing function has bounded variation, I exists. (A continuous integrand is Riemann–Stieltjes integrable against every bounded-variation integrator)

[L2]

For a nondecreasing integrator, Riemann-Stieltjes integrability is equivalent to the Darboux criterion; because g is continuous, for every ε>0 there is a partition P with UF(g,P)LF(g,P)<ε. (Darboux criterion for Riemann–Stieltjes integrability with a nondecreasing integrator)

[L3]

For every u<v, μF((u,v])=F(v)F(u). (Interval formulas and atoms for a Lebesgue-Stieltjes measure)

[L4]

The nonnegative integral agrees with the simple integral on simple functions, and the simple integral of jcjχEj is jcjμ(Ej). (The nonnegative integral agrees with the simple integral on simple functions, The integral of a nonnegative simple function)

[L5]

Continuous functions on R are Borel measurable. (Continuous functions on Euclidean spaces are Borel measurable)

[L6]

A measurable real function is integrable exactly when the integral of its absolute value is finite, and the Lebesgue integral is linear on L1. (Integrable real and complex functions, and their integrals, The Lebesgue integral is linear on L1(μ))

[L8]

Riemann-Stieltjes sums are S(g,F;P,ξ)=i=1mg(ξi)(F(ti)F(ti1)), and abgdF=J means that every tagged partition of sufficiently small mesh has sum within any prescribed ε>0 of J. (Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral)

[L9]

The Riemann-Stieltjes integral is linear in the integrand. (Linearity and interval additivity of the Riemann–Stieltjes integral)

Proof

technique · direct
1.1

Extend g to a continuous function g~:RR by setting g~(x)=g(a) for x<a, g~(x)=g(x) for x[a,b], and g~(x)=g(b) for x>b. Then [L5] makes g~ Borel measurable. Put h:=(B+g~)χ(a,b]. This is a nonnegative measurable function. Since 0h2Bχ(a,b], [L3], [L4], [L6], and [L7] show that h is μF-integrable. Let J:=ab(B+g)dF. By [L1], the integral J exists. The constant integrand B has the same Riemann-Stieltjes sum B(F(b)F(a)) for every tagged partition, so [L8] gives abBdF=B(F(b)F(a)). Therefore [L9] yields J=I+B(F(b)F(a)).

L1L3L4L5L6L8L9construct
1.2

Let ε>0. By [L2], choose a partition P0={a=t0<<tm=b} with UF(g,P0)LF(g,P0)<ε. By [L8], choose δ>0 such that every tagged partition of mesh below δ has Riemann-Stieltjes sum for B+g within ε of J. Let P={a=s0<<sn=b} be a refinement of P0 with mesh below δ. For each i put mi:=inf[si1,si]g,Mi:=sup[si1,si]g, and define nonnegative simple functions on R by P:=i=1n(B+mi)χ(si1,si],uP:=i=1n(B+Mi)χ(si1,si]. Then PhuP. Because each refined infimum is at least the corresponding coarse infimum and each refined supremum is at most the corresponding coarse supremum, the Stieltjes lower sum increases and the upper sum decreases under this refinement, so UF(g,P)LF(g,P)UF(g,P0)LF(g,P0)<ε. Also [L3] and [L4] give PdμF=B(F(b)F(a))+LF(g,P),uPdμF=B(F(b)F(a))+UF(g,P).

L2L3L4L8chooseconstruct
2.1

Fix any tagging ξ of P. Then PdμFhdμFuPdμF, and because mig(ξi)Mi on every subinterval, PdμFS(B+g,F;P,ξ)uPdμF. Hence both hdμF and S(B+g,F;P,ξ) lie in an interval of length UF(g,P)LF(g,P)<ε, so hdμFS(B+g,F;P,ξ)<ε.

step 1.2L7L8algebra
3.1

Because P<δ, [L8] gives S(B+g,F;P,ξ)J<ε. Combining this with step 2.1, hdμFJ<2ε. Since ε>0 was arbitrary, hdμF=J=I+B(F(b)F(a)).

step 1.1step 1.2step 2.1L8
4.1

Step 1.1 gives h=g~χ(a,b]+Bχ(a,b], and both summands are integrable by step 1.1. Therefore [L3] and [L6] yield (a,b]gdμF=hdμFBμF((a,b])=(I+B(F(b)F(a)))B(F(b)F(a))=I. This is exactly (a,b]gdμF=abgdF, so the two integrals agree.

step 1.1step 3.1L3L6

5 · Examples, counterexamples and false statements

None yet.

Sources