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

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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 55 results over 16 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. 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