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 , let be bounded and Riemann integrable, and write for its Riemann integral. Then there exist bounded Borel functions such that
In particular,
Facts & Assumptions
Given: The Axiom of Countable Choice, reals , a bounded Riemann integrable function with Riemann integral , and a real with for every .
Riemann's criterion says that for every real there is a partition of with . (Riemann's criterion: a bounded on is Darboux integrable if and only if for every real there is a partition with )
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)
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)
The nonnegative integral is monotone. (Monotonicity and nonnegative homogeneity of the nonnegative integral)
The nonnegative integral agrees with the simple integral on nonnegative simple functions, and the simple integral of is . (The nonnegative integral agrees with the simple integral on simple functions, The integral of a nonnegative simple function)
Monotone convergence holds for nonnegative measurable functions. (Monotone convergence for the integral)
Every interval of with any endpoint convention is Lebesgue measurable with its usual length. (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included)
A measurable real function is integrable exactly when the integral of its absolute value is finite, and the Lebesgue integral is linear on . (Integrable real and complex functions, and their integrals, The Lebesgue integral is linear on )
For every real there is a natural number with . (For every in a complete ordered field there is a natural with )
A bounded function is Riemann integrable with value exactly when it is Darboux integrable with the same value, and then every lower Darboux sum is at most and every upper Darboux sum is at least . (The Darboux and Riemann definitions agree: a bounded on is Darboux integrable with integral if and only if for every real there is a real such that for every tagged partition of mesh below , If on then for every partition ; in particular every constant function is integrable, with )
Proof
By [L1], choose recursively a refining sequence of partitions of such that for every : choose for , and once is chosen, let satisfy and put ; then [L2] preserves the inequality under refinement. For each , write and let and be the infimum and supremum of on . Define Each partition piece is a Borel subset of by [L3], so and are bounded Borel functions on . Also pointwise, while [L11] gives
Put and . Since , the last clause of [L4] makes Borel measurable; since are measurable, the infimum clause of [L4] makes Borel measurable. Step 1.1 gives . Now is a nonnegative simple function, so [L6] and [L8] give Because , [L7] yields the limit being the squeeze from step 1.1. Since , the constant function is integrable by [L6] and [L8], so step 1.1 and [L5], [L9] show that and
For each the function is nonnegative simple, and step 1.1 with [L6] and [L8] gives Because and , one has for every . So [L5] yields If that integral were positive, [L10] would give with , contradicting the displayed inequality. Therefore The same bound shows .
Since and both summands are integrable, [L9] and step 3.1 give Together with steps 2.1 and 3.1, this proves the existence of bounded Borel envelopes with the same Lebesgue integral .
Depends on
- Riemann's criterion: a bounded $f$ on $[a,b]$ is Darboux integrable if and only if for every real $\varepsilon > 0$ there is a partition $P$ with $U(f,P) - L(f,P) < \varepsilon$
- Refining a partition raises the lower Darboux sum and lowers the upper one, and every lower sum is at most every upper sum: $L(f,P) \le L(f,P') \le U(f,P') \le U(f,P)$ when $P'$ refines $P$, and $L(f,P) \le U(f,Q)$ for arbitrary partitions $P$ and $Q$; moreover the two changes are at most $2M(n' - n)\|P\|$
- The Darboux and Riemann definitions agree: a bounded $f$ on $[a,b]$ is Darboux integrable with integral $I$ if and only if for every real $\varepsilon > 0$ there is a real $\delta > 0$ such that $|S(f,P,\xi) - I| < \varepsilon$ for every tagged partition of mesh below $\delta$
- If $m \le f \le M$ on $[a,b]$ then $m(b-a) \le L(f,P) \le \underline{\int_a^b} f \le \overline{\int_a^b} f \le U(f,P) \le M(b-a)$ for every partition $P$; in particular every constant function is integrable, with $\int_a^b c = c(b-a)$
- The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra
- 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
- The Lebesgue integral is linear on $L^1(\mu)$
- Monotone convergence for the integral
- A box in $\mathbb{R}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure $\prod_{i<n}(b_i-a_i)$, whichever of its faces are included
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
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
- Richard F. Bass, Real Analysis for Graduate Students, Version 5.0, Section 9.1 and Exercise 9.6 (standard reference, not scraped)
- Richard L. Wheeden and Antoni Zygmund, Measure and Integral: An Introduction to Real Analysis, Section 5 (standard reference, not scraped)