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

Integration by parts for continuous factors with Riemann-integrable extensions of their interior derivatives

Statement

Let $a < b$ . Let $F, G : [a, b] \to R$ be continuous on $[a, b]$ and differentiable on $(a, b)$ . Suppose $f, g : [a, b] \to R$ are Riemann integrable and agree on $(a, b)$ with $F^{'}$ and $G^{'}$ , respectively. Then $F g$ and $f G$ are Riemann integrable and

$\int_{a}^{b} F (x) g (x) d x + \int_{a}^{b} f (x) G (x) d x = F (b) G (b) - F (a) G (a) .$

Equivalently,

$\int_{a}^{b} F g = [F G]_{a}^{b} - \int_{a}^{b} f G .$

No endpoint derivative of either factor is assumed.

Facts & Assumptions

Given: The functions in the statement.

[L1]

The product rule gives $(F G)^{'} = F^{'} G + F G^{'}$ wherever both derivatives exist (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L2]

Continuous functions on a compact interval are Riemann integrable, and products of Riemann-integrable functions are Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, If $f, g$ are integrable on $[a, b]$ then so are $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ and $\min (f, g)$ , and $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ ).

[L3]

The integral is linear on Riemann-integrable functions (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ).

[L4]

A continuous function with an interior derivative admitting an integrable extension satisfies Newton--Leibniz (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

Proof

technique · direct

1.1

The functions $F$ and $G$ are integrable, so [L2] makes $f G$ and $F g$ integrable; their sum $h : = f G + F g$ is integrable as well.

givenL2L3

1.2

The product $F G$ is continuous on $[a, b]$ , differentiable on $(a, b)$ , and [L1] gives $(F G)^{'} = f G + F g = h$ throughout the interior.

givenL1

2.1

Apply [L4] to $F G$ and its integrable derivative extension $h$ to obtain $\int_{a}^{b} h = F (b) G (b) - F (a) G (a)$ .

step 1.1step 1.2L4

3.1

Expanding the left side by [L3] gives the first displayed identity, and subtraction gives the equivalent form.

step 2.1L3algebra∎

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: 94 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. K. Hunter, An Introduction to Real Analysis, Theorem 12.10 (standard reference, not scraped)