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.

Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral

Statement

Let $a < b$ and $c < d$ . Suppose $g, h : [a, b] \times [c, d] \to R$ are continuous and, for every fixed $t \in [c, d]$ , the function $x \mapsto g (x, t)$ is differentiable on $(a, b)$ with derivative $h (x, t)$ . Define

$G (x) : = \int_{c}^{d} g (x, t) d t .$

Then $G$ is differentiable on $[a, b]$ as a function on that interval and

$G^{'} (x) = \int_{c}^{d} h (x, t) d t (x \in [a, b]) .$

At $a$ and $b$ the derivative is relative and one-sided. The derivative hypothesis is imposed only for interior parameter values; continuity of $h$ supplies its endpoint values.

Facts & Assumptions

Given: The rectangle and functions in the statement.

[L1]

A continuous real function on a compact interval is bounded and Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[L2]

A closed rectangle in $R^{2}$ is compact, and a continuous map from a compact metric space to $R$ is uniformly continuous (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L3]

The mean value theorem turns a difference quotient into a derivative value at an intermediate point (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[L4]

If two integrable functions differ uniformly by at most $η$ , then their integrals over $[c, d]$ differ by at most $η (d - c)$ (Uniformly close integrable functions have integrals differing by at most the interval length times their uniform error).

[L5]

Relative differentiability on a closed interval is convergence of the difference quotient over points of that interval (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

Proof

technique · epsilon-delta

1.1

For each $x$ , the slice $t \mapsto g (x, t)$ is continuous, so [L1] makes $G (x)$ well defined; the same applies to every slice of $h$ .

givenL1

1.2

Fix $x \in [a, b]$ and $ε > 0$ . Uniform continuity of $h$ on the compact rectangle gives $δ > 0$ such that $∣ h (y, t) - h (x, t) ∣ < ε / (d - c)$ whenever $∣ y - x ∣ < δ$ , uniformly in $t$ .

givenL2

2.1

Let $y \in [a, b]$ , $0 < ∣ y - x ∣ < δ$ . For every $t$ , [L3] applied to the parameter slice on the interval with endpoints $x, y$ gives a point $ξ_{t}$ strictly between them with $\frac{g (y, t) - g (x, t)}{y - x} = h (ξ_{t}, t)$ .

step 1.2L3

3.1

Because $∣ ξ_{t} - x ∣ < ∣ y - x ∣ < δ$ , step 1.2 gives $∣ \frac{g (y, t) - g (x, t)}{y - x} - h (x, t) ∣ < ε / (d - c)$ for every $t$ .

step 1.2step 2.1

4.1

The difference-quotient slice is continuous in $t$ and hence integrable. Linearity and [L4] now give $∣ \frac{G (y) - G (x)}{y - x} - \int_{c}^{d} h (x, t) d t ∣ < ε$ .

step 1.1step 3.1L4

5.1

Step 4.1 is precisely the relative derivative condition [L5]. It works with $y > x$ at $a$ , with $y < x$ at $b$ , and with both signs in the interior, proving the formula everywhere.

step 4.1L5∎

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: 139 results over 18 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, Theorem 9.1.1 (standard reference, not scraped)