Alphabeta MathHow 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.
Every bounded-variation function on a compact interval is Riemann integrable
Statement
Every real-valued function of bounded variation on a compact interval is Darboux, equivalently Riemann, integrable.
Facts & Assumptions
Given: A bounded-variation function .
Jordan decomposition writes with nondecreasing (Jordan decomposition for functions of bounded variation).
A monotone real function on a compact interval is integrable (A monotone function on is Riemann integrable: for the uniform partition into parts the upper minus lower sum telescopes to ).
Linear combinations of integrable functions are integrable and their integrals combine linearly (Integrable functions on form a set closed under sums and scalar multiples, and ).
Darboux integrability is the proper integral notion on (The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation ).
Proof
By [L1], and are nondecreasing; by [L2] both are integrable, and the constant function is integrable.
Linearity applied to makes integrable. The singleton interval follows from the zero-integral convention.
Depends on
- Jordan decomposition for functions of bounded variation
- A monotone function on $[a,b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $|f(b) - f(a)|\,(b-a)/\iota(N)$
- Integrable functions on $[a,b]$ form a set closed under sums and scalar multiples, and $\int_a^b(\lambda f+\mu g) = \lambda\int_a^b f + \mu\int_a^b g$
- 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$
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 58 results over 14 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
- William F. Trench, Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)