TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

For an integrable $f$ , the one-sided derivatives of $F (x) = \int_{a}^{x} f$ equal the corresponding one-sided limits of $f$ ; at a jump they are unequal

Statement

Let $a < b$ , let $f : [a, b] \to R$ be Riemann integrable, and put $F (x) = \int_{a}^{x} f$ .

If $c \in [a, b)$ and $\lim_{x \to c^{+}} f (x) = L_{+}$ , then the right derivative exists and $F_{+}^{'} (c) = L_{+}$ .
If $c \in (a, b]$ and $\lim_{x \to c^{-}} f (x) = L_{-}$ , then the left derivative exists and $F_{-}^{'} (c) = L_{-}$ .

In particular, if both one-sided limits exist at an interior point and are unequal, then $F$ is not differentiable there. The value $f (c)$ itself is irrelevant to both conclusions.

Facts & Assumptions

Given: The integrable $f$ , its integral function $F$ , and the indicated one-sided limits.

[L1]

Integral additivity gives $F (y) - F (c) = \int_{c}^{y} f$ for all $c, y \in [a, b]$ , with oriented limits (The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ , For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[L2]

The right-limit condition says that for every $ε > 0$ , $∣ f (x) - L_{+} ∣ < ε$ throughout a sufficiently short interval to the right of $c$ ; the left version is analogous (The left and right limits of $f$ at $c$ , as limits of the restrictions of $f$ to $A \cap (- \infty, c)$ and $A \cap (c, \infty)$ ).

[L3]

If $∣ g ∣ \leq M$ on an interval of length $ℓ$ , then $∣ \int g ∣ \leq M ℓ$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

Proof

technique · epsilon-delta

1.1

Assume the right limit exists and fix $ε > 0$ . By [L2], choose $δ > 0$ so that $∣ f (x) - L_{+} ∣ < ε$ whenever $c < x < c + δ$ within $[a, b]$ .

givenL2

1.2

For the left limit, take $h < 0$ , rewrite the same quotient using the oriented integral over $[c + h, c]$ , and apply [L2] and [L3]; its limit is $L_{-}$ .

givenL1L2L3

2.1

For $0 < h < δ$ with $c + h \leq b$ , [L1] and linearity give $\frac{F (c + h) - F (c)}{h} - L_{+} = \frac{1}{h} \int_{c}^{c + h} (f - L_{+})$ .

step 1.1L1algebra

3.1

By [L3], the absolute value in step 2.1 is at most $ε$ . Hence the right difference quotient tends to $L_{+}$ .

step 1.1step 2.1L3

4.1

At an interior point a two-sided derivative would have to equal both one-sided derivatives, so unequal $L_{+}$ and $L_{-}$ preclude it. Neither estimate refers to $f (c)$ .

step 3.1step 1.2∎

Depends on

Used by

A bounded increasing integrand discontinuous at every rational has an integral function nondifferentiable at every rational in (0,1) Example

Dependency tree · two levels

25 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

J. K. Hunter, An Introduction to Real Analysis, Theorem 12.4 (standard reference, not scraped)

For an integrable ff, the one-sided derivatives of F(x)=∫axfF(x)=∫ax​f equal the corresponding one-sided limits of ff; at a jump they are unequal