CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Assuming Countable Choice, the integral function of a Riemann-integrable function is Lipschitz and differentiable almost everywhere, with derivative equal to the integrand there

Statement

Assume the Axiom of Countable Choice. Let $a < b$ , let $f : [a, b] \to R$ be Riemann integrable, and let

$F (x) : = \int_{a}^{x} f .$

Then $F$ is Lipschitz on $[a, b]$ . If $D$ is the set of discontinuities of $f$ , then $D$ has measure zero and

$F^{'} (x) = f (x) (x \in [a, b] ∖ D) .$

Thus the set of points where $F^{'}$ fails to exist or differs from $f$ is contained in a set of measure zero. At $a$ and $b$ , the displayed derivative is the relative one-sided derivative on $[a, b]$ .

Facts & Assumptions

Given: Reals $a < b$ , an integrable $f : [a, b] \to R$ , its integral function $F$ , and Countable Choice.

[L1]

An integrable $f$ is bounded, and if $∣ f ∣ \leq K$ then its integral function satisfies $∣ F (y) - F (x) ∣ \leq K ∣ y - x ∣$ (The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous).

[L2]

Assuming Countable Choice, a bounded function is Riemann integrable if and only if its discontinuity set has measure zero (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).

[L3]

If $f$ is integrable and continuous at $c \in [a, b]$ , then its integral function is differentiable at $c$ and $F^{'} (c) = f (c)$ , with relative endpoint derivatives (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

Proof

technique · direct

1.1

Integrability supplies a bound $∣ f ∣ \leq K$ , so $F$ is Lipschitz by [L1].

givenL1

1.2

The discontinuity set $D$ has measure zero by the forward implication of [L2], whose stated proof is the sole use of Countable Choice.

givenL2

2.1

Every $x \in [a, b] ∖ D$ is a continuity point of $f$ , so [L3] gives $F^{'} (x) = f (x)$ there, including the relative derivative at an endpoint outside $D$ .

step 1.2L3

3.1

Hence every point at which the derivative conclusion fails lies in $D$ , and that containing set has measure zero.

step 1.2step 2.1∎

Depends on

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: 127 results over 20 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

J. Lebl, Basic Analysis I & II, Section 5.3 (standard reference, not scraped)