Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28
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.

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

Depends on

Used by

Dependency tree · two levels

66 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