TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-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.

Lebesgue's criterion for Riemann integrability: a bounded $f$ on $[a, b]$ is Riemann integrable if and only if its set of discontinuities has measure zero

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be bounded (Lower bound, bounded below, bounded set) and let

$D : = {x \in [a, b] : f is discontinuous at x}$

(Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, Discontinuity of $f$ at a point of its domain, and its classification: removable discontinuity, jump discontinuity and essential discontinuity, equivalently Rudin's discontinuities of the first and of the second kind). Then

$f is Riemann integrable on [a, b] ⟺ D has measure zero$

(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$ , Measure zero (a countable cover by intervals of total length below every $ε$ ) and content zero (a finite such cover)).

The choice cost, named. The implication from integrability to $D$ being null uses the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) exactly once, through A countable union of measure-zero sets has measure zero, by countable choice at step 7.1: $D$ is exhibited as the union of a sequence of null sets. The converse implication, from $D$ null to integrability, is a theorem of ZF: it uses no choice principle at all.

"Measure zero" here is the cover condition of Measure zero (a countable cover by intervals of total length below every $ε$ ) and content zero (a finite such cover), namely that for every $ε > 0$ there is a sequence of intervals covering $D$ of total length at most $ε$ . No outer measure, no measurable set and no Lebesgue integral is used or needed; the criterion is a statement about interval covers throughout.

Facts & Assumptions

Given: Reals $a < b$ , a bounded $f : [a, b] \to R$ , a real $M_{+} > 0$ with $∣ f (x) ∣ \leq M_{+}$ for every $x \in [a, b]$ , and $D$ as in the Statement.

[A1]

The Axiom of Countable Choice, used only where [L11] is invoked (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L1]

For a partition $P = (n, t)$ of $[a, b]$ : $n \geq 1$ , $Δ_{i} = t_{i + 1} - t_{i} > 0$ , $\sum_{i < n} Δ_{i} = b - a$ , $I_{i} = [t_{i}, t_{i + 1}] \subseteq [a, b]$ , and appending a point $y > t_{n}$ to a partition of $[a, t_{n}]$ gives a partition of $[a, y]$ whose subintervals are the old ones together with $[t_{n}, y]$ (Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).

[L2]

$U (f, P) - L (f, P) = \sum_{i < n} (M_{i} - m_{i}) Δ_{i}$ , $M_{i} - m_{i} = ω_{f} (I_{i})$ , and $0 \leq M_{i} - m_{i} \leq 2 M_{+}$ (For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ , The oscillation $ω_{f} (S) = \sup {∣ f (x) - f (y) ∣ : x, y \in S}$ of $f$ on a set and the oscillation $ω_{f} (c) = \inf_{δ > 0} ω_{f} (A \cap N_{δ} (c))$ at a point, both taken in the extended reals).

[L3]

Riemann's criterion: a bounded $f$ is integrable if and only if for every real $ε > 0$ there is a partition $P$ 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) < ε$ ).

[L4]

Oscillation: $ω_{f} (S) \leq ω_{f} (T)$ for $S \subseteq T \subseteq [a, b]$ ; $0 \leq ω_{f} (x) \leq ω_{f} ([a, b] \cap N_{ρ} (x))$ for every real $ρ > 0$ and every $x \in [a, b]$ ; $ω_{f} (x)$ is the infimum of those values over $ρ > 0$ ; and since $f$ is bounded every one of these values is a real number in $[0, 2 M_{+}]$ (The oscillation $ω_{f} (S) = \sup {∣ f (x) - f (y) ∣ : x, y \in S}$ of $f$ on a set and the oscillation $ω_{f} (c) = \inf_{δ > 0} ω_{f} (A \cap N_{δ} (c))$ at a point, both taken in the extended reals, The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined, The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L5]

$f$ is continuous at $x \in [a, b]$ if and only if $ω_{f} (x) = 0$ ; hence $D = {x \in [a, b] : ω_{f} (x) > 0}$ ( $f : A \to R$ is continuous at $c \in A$ if and only if $ω_{f} (c) = 0$ , Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L6]

For every real $σ > 0$ there is a closed $G \subseteq R$ with ${x \in [a, b] : ω_{f} (x) \geq σ} = [a, b] \cap G$ (For every real $ε > 0$ the set ${x \in A : ω_{f} (x) \geq ε}$ is the intersection with $A$ of a closed subset of $R$ ; in particular it is closed in $R$ when $A = R$ ).

[L7]

A subset of $R$ is compact exactly when it is closed and bounded; $[a, b]$ is closed and bounded; an intersection of closed sets is closed; every open interval is an open set (A subset of $R$ is compact if and only if it is closed and bounded, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset, Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Arbitrary unions and finite intersections of open subsets of $R$ are open, and dually for closed sets, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Lower bound, bounded below, bounded set).

[L8]

$A$ has content zero when for every real $τ > 0$ there are $m \in N$ and reals $c_{0} \leq e_{0}, \dots, c_{m} \leq e_{m}$ with $A \subseteq ⋃_{j \leq m} [c_{j}, e_{j}]$ and $\sum_{j \leq m} (e_{j} - c_{j}) \leq τ$ ; $A$ has measure zero when the same holds with a sequence of intervals and every partial total length at most $τ$ ; a subset of a null set is null (Measure zero (a countable cover by intervals of total length below every $ε$ ) and content zero (a finite such cover)).

[L9]

A set of content zero has measure zero (A set of content zero has measure zero), and for a compact set the two notions coincide (For a compact subset of $R$ , measure zero and content zero coincide).

[L10]

For every real $η > 0$ there is a natural $k \geq 1$ with $1 / ι (k) < η$ ; $ι (k) > 0$ for $k \geq 1$ , $ι$ is nonnegative and nondecreasing on $N$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L11]

Assuming [A1], the union of a sequence of null subsets of $R$ is null (A countable union of measure-zero sets has measure zero, by countable choice, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L12]

Finite sums: splitting, additivity, scaling, monotonicity in the terms, and telescoping (Finite sums and finite products, by recursion, Laws of finite sums and finite products). Also the interchange of two finite sums, $\sum_{i < n} \sum_{j < p} c_{i, j} = \sum_{j < p} \sum_{i < n} c_{i, j}$ for any doubly indexed family of reals; below it is applied with $p : = m + 1$ , since $\sum_{j \leq m}$ abbreviates $\sum_{j < m + 1}$ . That identity is not one of the six clauses of Laws of finite sums and finite products and is therefore proved here, by induction on $p$ with $n$ held fixed (The principle of mathematical induction). At $p = 0$ each inner sum $\sum_{j < 0} c_{i, j}$ is $0$ by the recursion clause of Finite sums and finite products, by recursion, so the left side is $\sum_{i < n} 0 = 0$ by clause 2 of Laws of finite sums and finite products taken with $λ = 0$ , while the right side is an empty sum and so is $0$ as well. Passing from $p$ to $p + 1$ , the recursion clause and clause 1 of Laws of finite sums and finite products give $\sum_{i < n} \sum_{j < p + 1} c_{i, j} = \sum_{i < n} (\sum_{j < p} c_{i, j} + c_{i, p}) = \sum_{i < n} \sum_{j < p} c_{i, j} + \sum_{i < n} c_{i, p}$ , which by the induction hypothesis is $\sum_{j < p} \sum_{i < n} c_{i, j} + \sum_{i < n} c_{i, p} = \sum_{j < p + 1} \sum_{i < n} c_{i, j}$ , again by the recursion clause.

[L13]

Every nonempty subset of $N$ has a least element (The well-ordering principle); every nonempty subset of $R$ bounded above has a supremum (Complete ordered field (least-upper-bound property)).

[L14]

Ordered-field arithmetic and the absolute value: adding a constant and multiplying by a positive quantity preserve an inequality; the order is total and transitive; an open interval is order-convex (Basic properties of the absolute value, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property), Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Proof

technique · direct

1.1

For a real $σ > 0$ put $E_{σ} : = {x \in [a, b] : ω_{f} (x) \geq σ}$ . By [L5], $E_{σ} \subseteq D$ for every $σ > 0$ .

L4L5construct

2.1

Each $E_{σ}$ has content zero, assuming $f$ integrable. Let $σ > 0$ and $τ > 0$ be real. By [L3] fix a partition $P = (n, t)$ with $U (f, P) - L (f, P) < σ τ \cdot 2^{- 1}$ . Let $B : = {i < n : (t_{i}, t_{i + 1}) \cap E_{σ} \neq \emptyset}$ and put $χ_{i} : = 1$ for $i \in B$ and $χ_{i} : = 0$ otherwise.

step 1.1L3L14chooseconstruct

2.2

The exhaustion of $D$ . Put $σ_{k} : = 1 / ι (k + 1)$ for $k \in N$ , a positive real by [L10]. Then $D = ⋃_{k \in N} E_{σ_{k}}$ . For the inclusion from left to right, let $x \in D$ , so $ω_{f} (x) > 0$ by [L5] and $ω_{f} (x)$ is a real by [L4]; if $ω_{f} (x) \geq 1 = σ_{0}$ then $x \in E_{σ_{0}}$ , and otherwise [L10] gives a natural $k + 1 \geq 1$ with $1 / ι (k + 1) < ω_{f} (x)$ , so $x \in E_{σ_{k}}$ . For the reverse inclusion, $x \in E_{σ_{k}}$ gives $ω_{f} (x) \geq σ_{k} > 0$ , hence $x \in D$ by [L5].

step 1.1L4L5L10L14

2.3

The converse; this half of the proof is steps 2.3, 3.2, 4.2, 5.2, 6.2, 7.2, 8.1, 9.1, 10.1, 11.1, 12.1 and 13.1, and its symbols are its own. Assume $D$ null and let a real $ε > 0$ be given. Put $σ^{'} : = ε \cdot (2 (b - a))^{- 1}$ and $τ^{'} : = ε \cdot (8 M_{+})^{- 1}$ , both positive by [L14]. By step 1.1 and [L8], $E_{σ^{'}} \subseteq D$ is null.

step 1.1givenL8L14

3.1

For $i \in B$ one has $M_{i} - m_{i} \geq σ$ : fix $x \in (t_{i}, t_{i + 1}) \cap E_{σ}$ ; since $(t_{i}, t_{i + 1})$ is open there is a real $ρ > 0$ with $N_{ρ} (x) \subseteq (t_{i}, t_{i + 1})$ , so $[a, b] \cap N_{ρ} (x) \subseteq I_{i}$ and [L4] gives $σ \leq ω_{f} (x) \leq ω_{f} ([a, b] \cap N_{ρ} (x)) \leq ω_{f} (I_{i}) = M_{i} - m_{i}$ by [L2].

step 2.1L1L2L4L7choose

3.2

$E_{σ^{'}}$ is compact: by [L6] there is a closed $G$ with $E_{σ^{'}} = [a, b] \cap G$ , an intersection of two closed sets, hence closed; and $E_{σ^{'}} \subseteq [a, b]$ is bounded. So [L7] applies.

step 2.3L6L7

4.1

Hence $σ χ_{i} Δ_{i} \leq (M_{i} - m_{i}) Δ_{i}$ for every $i < n$ , the case $i \notin B$ because both $M_{i} - m_{i} \geq 0$ and $Δ_{i} > 0$ . Summing and using [L12] and [L2]: $σ \sum_{i < n} χ_{i} Δ_{i} \leq U (f, P) - L (f, P) < σ τ \cdot 2^{- 1}$ , so $λ : = \sum_{i < n} χ_{i} Δ_{i} < τ \cdot 2^{- 1}$ .

step 2.1step 3.1L2L12L14

4.2

By [L9] applied to the compact null set $E_{σ^{'}}$ , it has content zero, so by [L8] there are $m \in N$ and reals $c_{0} \leq e_{0}, \dots, c_{m} \leq e_{m}$ with $E_{σ^{'}} \subseteq ⋃_{j \leq m} [c_{j}, e_{j}]$ and $\sum_{j \leq m} (e_{j} - c_{j}) \leq τ^{'} \cdot 2^{- 1}$ . Put $μ : = τ^{'} \cdot (4 (ι (m) + 1))^{- 1} > 0$ and $O_{j} : = (c_{j} - μ, e_{j} + μ)$ , an open interval containing $[c_{j}, e_{j}]$ , of length $(e_{j} - c_{j}) + 2 μ$ . Then $\sum_{j \leq m} ((e_{j} - c_{j}) + 2 μ) \leq τ^{'} \cdot 2^{- 1} + 2 μ (ι (m) + 1) = τ^{'} \cdot 2^{- 1} + τ^{'} \cdot 2^{- 1} = τ^{'}$ , by [L12] and [L10].

step 2.3step 3.2L8L9L10L12L14construct

5.1

$E_{σ}$ is covered by the finite list of $2 n + 1$ closed intervals $[p_{j}, q_{j}]$ , $j \leq 2 n$ , defined by $[p_{j}, q_{j}] : = [t_{j}, t_{j + 1}]$ for $j < n$ with $j \in B$ , $[p_{j}, q_{j}] : = [a, a]$ for $j < n$ with $j \notin B$ , and $[p_{j}, q_{j}] : = [t_{j - n}, t_{j - n}]$ for $n \leq j \leq 2 n$ : indeed a point of $E_{σ}$ lies in $[a, b]$ , hence is one of $t_{0}, \dots, t_{n}$ or lies in some $(t_{i}, t_{i + 1})$ , and in the latter case $i \in B$ . Its total length is $\sum_{j \leq 2 n} (q_{j} - p_{j}) = \sum_{i < n} χ_{i} Δ_{i} + 0 = λ < τ$ , by splitting the sum at $n$ ([L12]).

step 2.1step 4.1L1L12L14construct

5.2

The family of good intervals. Let $W$ be the set of all open intervals $(u, v)$ with $u < v$ such that either $(u, v) \subseteq O_{j}$ for some $j \leq m$ , or $ω_{f} ([a, b] \cap (u, v)) < σ^{'}$ . Every $x \in [a, b]$ lies in a member: if $x \in E_{σ^{'}}$ then $x \in [c_{j}, e_{j}] \subseteq O_{j}$ for some $j \leq m$ by step 4.2, and $O_{j}$ is itself a member; and if $x \notin E_{σ^{'}}$ then $ω_{f} (x) < σ^{'}$ , so by [L4] some real $ρ > 0$ has $ω_{f} ([a, b] \cap N_{ρ} (x)) < σ^{'}$ , and $N_{ρ} (x) = (x - ρ, x + ρ)$ is a member containing $x$ .

step 4.2L4L7L14construct

6.1

As $τ > 0$ was arbitrary, $E_{σ}$ has content zero by [L8], hence measure zero by [L9]; this used only that $f$ is integrable.

step 2.1step 5.1L8L9

6.2

Cousin's construction: a partition each of whose subintervals lies in a member of $W$ . Let $S$ be the set of $y \in (a, b]$ such that some partition of $[a, y]$ has every subinterval contained in a member of $W$ . $S$ is nonempty: by step 5.2 fix $(α, β) \in W$ with $a \in (α, β)$ and put $y_{0} : = \min {(a + b) \cdot 2^{- 1}, (a + β) \cdot 2^{- 1}}$ , so $a < y_{0} \leq b$ , $y_{0} < β$ and $α < a$ ; the one-subinterval partition of $[a, y_{0}]$ has $[a, y_{0}] \subseteq (α, β)$ , so $y_{0} \in S$ . Also $S$ is bounded above by $b$ , so $s : = \sup S$ exists by [L13] and $a < y_{0} \leq s \leq b$ .

step 5.2L1L13L14choose

7.1

Integrability implies $D$ null. Assume $f$ integrable. By step 6.1 each $E_{σ_{k}}$ is null, and $k \mapsto E_{σ_{k}}$ is a sequence of subsets of $R$ , so [L11] applies and $⋃_{k} E_{σ_{k}} = D$ is null by step 2.2. This is the only use of [A1] in the proof.

step 6.1step 2.2A1L11

7.2

$s = b$ . By step 5.2 fix $(α^{'}, β^{'}) \in W$ with $s \in (α^{'}, β^{'})$ . Since $\sup S = s > α^{'}$ there is $x \in S$ with $x > α^{'}$ , and $x \leq s$ . Suppose $s < b$ and choose a real $y$ with $s < y < \min {b, β^{'}}$ , possible because $s < b$ and $s < β^{'}$ . Then $α^{'} < x \leq s < y < β^{'}$ , so $[x, y] \subseteq (α^{'}, β^{'})$ , and appending $y$ to a partition of $[a, x]$ witnessing $x \in S$ gives one for $[a, y]$ by [L1]; hence $y \in S$ with $y > \sup S$ , which is impossible.

step 6.2L1L13L14choose

8.1

$b \in S$ . By step 5.2 fix $(α^{''}, β^{''}) \in W$ with $b \in (α^{''}, β^{''})$ . Since $\sup S = b > α^{''}$ there is $x \in S$ with $x > α^{''}$ and $x \leq b$ . If $x = b$ there is nothing to prove; otherwise $α^{''} < x < b < β^{''}$ gives $[x, b] \subseteq (α^{''}, β^{''})$ , and appending $b$ as in step 7.2 puts $b$ in $S$ . So there is a partition $P^{'} = (n^{'}, t^{'})$ of $[a, b]$ , with subintervals $I_{i}^{'}$ and lengths $Δ_{i}^{'}$ for $i < n^{'}$ , every subinterval of which lies in a member of $W$ .

step 5.2step 7.2L1L13L14choose

9.1

Good and bad subintervals. Write $M_{i}^{'} : = \sup f [I_{i}^{'}]$ and $m_{i}^{'} : = \inf f [I_{i}^{'}]$ . Call $i < n^{'}$ good when $I_{i}^{'} \subseteq W$ for some $W = (u, v) \in W$ with $ω_{f} ([a, b] \cap (u, v)) < σ^{'}$ , and bad otherwise. For a good $i$ , $I_{i}^{'} \subseteq [a, b] \cap W$ , so $M_{i}^{'} - m_{i}^{'} = ω_{f} (I_{i}^{'}) \leq ω_{f} ([a, b] \cap W) < σ^{'}$ by [L2] and [L4]. For a bad $i$ , step 8.1 supplies a member containing $I_{i}^{'}$ , and it is not of the second kind, so $I_{i}^{'} \subseteq O_{j}$ for some $j \leq m$ .

step 8.1L1L2L4

10.1

Bounding the bad lengths. For $j \leq m$ put $J_{j} : = {i < n^{'} : c_{j} - μ \leq t_{i}^{'} and t_{i + 1}^{'} \leq e_{j} + μ}$ and $h_{i}^{j} : = Δ_{i}^{'}$ for $i \in J_{j}$ , $h_{i}^{j} : = 0$ otherwise; a bad $i$ lies in some $J_{j}$ by step 9.1. Each $J_{j}$ consists of consecutive indices, since $i < i^{†} < i^{‡}$ with $i, i^{‡} \in J_{j}$ gives $c_{j} - μ \leq t_{i}^{'} \leq t_{i^{†}}^{'}$ and $t_{i^{†} + 1}^{'} \leq t_{i^{‡} + 1}^{'} \leq e_{j} + μ$ .

step 9.1L1L14construct

11.1

$\sum_{i < n^{'}} h_{i}^{j} \leq (e_{j} - c_{j}) + 2 μ$ for each $j \leq m$ : the sum is $0$ when $J_{j} = \emptyset$ ; otherwise let $p : = \min J_{j}$ and let $q$ be the least natural with $q > p$ and $q \notin J_{j}$ , which exists by [L13] since $n^{'} \notin J_{j}$ , so that $J_{j} = {i : p \leq i < q}$ by step 10.1. Splitting the sum at $p$ and at $q$ and discarding the vanishing outer parts, then telescoping ([L12]), gives $\sum_{i < n^{'}} h_{i}^{j} = \sum_{i = p}^{q - 1} Δ_{i}^{'} = t_{q}^{'} - t_{p}^{'} \leq (e_{j} + μ) - (c_{j} - μ)$ , using $p \in J_{j}$ and $q - 1 \in J_{j}$ .

step 10.1L12L13L14

12.1

Put $β_{i} : = Δ_{i}^{'}$ for bad $i$ and $β_{i} : = 0$ for good $i$ . Then $β_{i} \leq \sum_{j \leq m} h_{i}^{j}$ pointwise by step 10.1, all terms being nonnegative, so by [L12] and step 11.1, $\sum_{i < n^{'}} β_{i} \leq \sum_{j \leq m} \sum_{i < n^{'}} h_{i}^{j} \leq \sum_{j \leq m} ((e_{j} - c_{j}) + 2 μ) \leq τ^{'}$ , the last step by step 4.2.

step 4.2step 10.1step 11.1L12L14

13.1

For every $i < n^{'}$ , $(M_{i}^{'} - m_{i}^{'}) Δ_{i}^{'} \leq σ^{'} Δ_{i}^{'} + 2 M_{+} β_{i}$ : for good $i$ by step 9.1 and $β_{i} \geq 0$ , for bad $i$ by $M_{i}^{'} - m_{i}^{'} \leq 2 M_{+}$ from [L2] and $β_{i} = Δ_{i}^{'}$ . Summing over $i < n^{'}$ and using [L12], [L1] and step 12.1: $U (f, P^{'}) - L (f, P^{'}) \leq σ^{'} (b - a) + 2 M_{+} τ^{'} = ε \cdot 2^{- 1} + ε \cdot 4^{- 1} < ε$ .

step 2.3step 9.1step 12.1L1L2L12L14

14.1

The real $ε > 0$ of step 2.3 was arbitrary and step 13.1 produced a partition with $U - L < ε$ , so $f$ is integrable by [L3]. With step 7.1 this proves both implications, and the criterion is established; the forward half is steps 1.1, 2.1, 2.2, 3.1, 4.1, 5.1, 6.1 and 7.1, working with $σ, τ, P, B, χ, λ$ , and the converse half is the steps named in step 2.3, working with $σ^{'}, τ^{'}, P^{'}, W, S$ .

step 7.1step 2.3step 13.1L3∎

Remarks

What the two halves cost. The forward half is a single application of Riemann's criterion for each threshold $σ$ , plus the countable union; the backward half is where all the work is, and it is entirely a covering argument: the bad set is compact and null, hence of content zero, hence coverable by finitely many open intervals of small total length, and the rest of $[a, b]$ is chopped up by Cousin's construction into pieces of oscillation below $σ$ .
Why Cousin's construction and not a Lebesgue number. Step 6.2 to step 8.1 build the partition directly from the completeness of $R$ : the set of right endpoints reachable by a good partition is nonempty and bounded, and its supremum is shown to be $b$ and to be attained. This uses no sequence, no subsequence and no choice, whereas the usual Lebesgue-number argument selects a bad interval for each $n$ and then extracts a convergent subsequence, which costs countable choice. Since the whole point of this item's choice ledger is that the backward implication is a ZF theorem, the choice-free route is the one taken.
The superlevel sets, not the discontinuity set, are what is covered. $D$ itself is in general not closed, so For a compact subset of $R$ , measure zero and content zero coincide does not apply to it; each $E_{σ}$ is closed in $[a, b]$ (For every real $ε > 0$ the set ${x \in A : ω_{f} (x) \geq ε}$ is the intersection with $A$ of a closed subset of $R$ ; in particular it is closed in $R$ when $A = R$ ) and bounded, and that is exactly the hypothesis needed. The passage back from the $E_{σ_{k}}$ to $D$ is step 2.2, and it is where the countable union appears.
The exhaustion $D = ⋃_{k} E_{1 / ι (k + 1)}$ is derived here, and it is also claim 1 of For $f : A \to R$ the set of points of $A$ at which $f$ is discontinuous is the intersection with $A$ of an $F_{σ}$ subset of $R$ , and the set of points at which $f$ is continuous is the intersection with $A$ of a $G_{δ}$ subset; for $A = R$ the two sets are $F_{σ}$ and $G_{δ}$ outright. When this proof was written that theorem stated only the descriptive form — $D$ as the trace on the domain of an $F_{σ}$ subset of $R$ — which is not the pointwise identity step 2.2 needs, so the identity was derived inline from $f : A \to R$ is continuous at $c \in A$ if and only if $ω_{f} (c) = 0$ and the Archimedean property. The exhaustion has since been stated there as claim 1, precisely because several items were quoting it from a theorem that did not assert it. The inline derivation is retained because it is three lines and keeps this item's choice ledger readable in one place; citing claim 1 instead would be equally correct.
Both directions are sharp in the obvious sense. The indicator of the Cantor set is discontinuous on an uncountable null set and is integrable; the indicator of the Smith-Volterra-Cantor set is discontinuous on a nowhere dense set that is not null and is not integrable (FALSE: a bounded function on $[a, b]$ is Riemann integrable exactly when its set of discontinuities is nowhere dense). So neither cardinality nor category decides integrability; only measure does.

Depends on

Used by

Dependency tree · two levels

87 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

Riemann integral (Wikipedia) (standard reference, not scraped)
Lebesgue's criterion for Riemann integrability (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 11 (standard reference, not scraped)
J. Hunter, Chapter 11: The Riemann Integral (standard reference, not scraped)
M. Wodzicki, The Riemann Integral (standard reference, not scraped)

Lebesgue's criterion for Riemann integrability: a bounded ff on [a,b][a,b] is Riemann integrable if and only if its set of discontinuities has measure zero