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.
If are differentiable on with integrable, then
Statement
Let be reals and let be differentiable at every point of as functions on (The derivative of at a point that is a limit point of , and differentiability on a set). Suppose and are integrable on (The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation ). Then and are integrable and
The integrability of and is a hypothesis, not a formality. Without it the two integrals in the display need not exist at all, and the identity is then not false but ill-formed; that is the false statement that deletes it on the companion page. The hypothesis is automatic when and are continuously differentiable, since a continuous function on is integrable (A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion).
Statement references
Facts & Assumptions
Given: Reals and functions , differentiable at every point of , with and integrable on .
Product rule: if and are differentiable at then so is , with (Sums, scalar multiples, products and quotients: , , , and when , claim 3); every point of is a limit point of it, so the rule applies at every point (Limit point, isolated point, adherent point, derived set, and dense subset of , Intervals of : the nine order-convex forms, nondegeneracy, and length, The derivative of at a point that is a limit point of , and differentiability on a set).
A function differentiable at every point of is continuous there (A function differentiable at is continuous at , Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
A continuous function on is integrable there (A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion).
A product of two integrable functions on is integrable (If are integrable on then so are , , , and , and , claim 1).
Sums of integrable functions are integrable, and (Integrable functions on form a set closed under sums and scalar multiples, and ).
If is differentiable at every point of with integrable there, then (The second fundamental theorem: if is differentiable on with and is integrable, then ).
Proof
and are continuous on by [L2], hence integrable there by [L3].
is differentiable at every point of with by [L1].
and are integrable on by [L4], being products of the integrable with and of with the integrable .
Hence is integrable by [L5], and .
By [L6] applied to , .
Comparing steps 3.1 and 4.1 and subtracting gives .
Remarks
-
Step 2.1 is the step usually skipped, and it is why the hypotheses are what they are. The identity is an application of the second fundamental theorem to , and that theorem needs to be integrable. Integrability of and plus continuity of and delivers it, through the product clause of If are integrable on then so are , , , and , and ; nothing weaker is used, and nothing weaker is claimed to suffice.
-
The boundary term is exactly the increment of . Writing the identity as makes the symmetry in and visible and is the form worth remembering.
-
Discrete counterpart. Abel's summation by parts (Abel summation by parts: with one has for every ) is the same manipulation for finite sums, and it is what Bonnet's second mean value theorem: for monotone and integrable on there is with below uses in place of this theorem, precisely because that theorem assumes no differentiability.
-
Forward reference, orientation only. The false statement that deletes the integrability hypothesis is FALSE: if and are differentiable on then on the companion page; nothing above depends on it.
Depends on
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- A function differentiable at $c$ is continuous at $c$
- 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 $\lvert f\rvert$, $f^{2}$, $fg$, $\max(f,g)$ and $\min(f,g)$, and $\bigl\lvert\int_a^b f\bigr\rvert \le \int_a^b\lvert f\rvert$
- Integrable functions on $[a,b]$ form a set closed under sums and scalar multiples, and $\int_a^b(\lambda f+\mu g) = \lambda\int_a^b f + \mu\int_a^b g$
- The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$, and differentiability on a set
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- The lower and upper Darboux integrals of a bounded $f$ on $[a,b]$ as $\sup_P L(f,P)$ and $\inf_P U(f,P)$, Darboux integrability as their equality, and the notation $\int_a^b f$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$
Used by
- Sharp Gaussian asymptotics under a vanishing largest weight Corollary
- Shifted character observables p_ρ^# and profile moments p̃ₖ Definition
- Characteristic function of a gaussian law Example
- Conditional density of a bivariate normal law Example
- Density inversion for a triangular characteristic function Example
- Gaussian-kernel moments and pointwise constants Example
- Independent sums via characteristic functions Example
- L² forcing defines an H⁻¹ functional Example
- One-dimensional Dirichlet Green kernel on an interval Example
- The Fourier series of a sawtooth and the Basel sum Example
- The weak Dirichlet Poisson problem on an interval Example
- FALSE: if u and v are differentiable on [a,b] then ∫ₐᵇ uv' = u(b)v(b)-u(a)v(a)-∫ₐᵇ u'v False statement
- A characteristic function that is Gaussian near zero is globally Gaussian Lemma
- A finite-array normal limit from vanishing fourth moments Lemma
- A normal variable has finite fourth moment Lemma
- An integrable C² density with bounded Hessian is bounded Lemma
- Backward uniqueness for the heat equation on a bounded interval Lemma
- Binet integral identity for the right-half-plane log-Gamma branch Lemma
- Cartesian Gaussian moments and exponent-parameter derivatives Lemma
- Characteristic function of a normal law Lemma
- Compactly supported Gaussian mixtures admit logarithmic-size finite approximations Lemma
- Complex integration by parts on intervals and decaying lines Lemma
- Density normal laws and square-summable Gaussian series under countable choice Lemma
- Finite Gaussian increment comparison Lemma
- Fresnel whole-line moment from the damped complex Gaussian Lemma
- Gaussian convolution has second-order KL and log-square error Lemma
- Gaussian density integrals for supplied length measures Lemma
- Gaussian even moments for Brownian increments Lemma
- Legendre polynomials have explicit norms and weighted derivative orthogonality Lemma
- Local stationary expansion for a quadratic phase Lemma
- Midpoint panel error kernel and second-derivative bound Lemma
- Moment recurrence for the scaled complementary error function Lemma
- One-dimensional quadratic oscillatory amplitude bound Lemma
- Peano kernel identity for one Simpson panel Lemma
- Planar Brownian annular exit probability Lemma
- Second-order kernel convolution has an L² bias bound Lemma
- Simultaneous initialization estimates for the Du architectures Lemma
- Smooth torus test functions have rapidly convergent Fourier pairings Lemma
- The sharp Dirichlet Poincare inequality on an interval Lemma
- The sine integral under Countable Choice: uniform bounds and the value pi/2 Lemma
…and 22 more results.
Dependency tree · two levels
55 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
- Integration by parts (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 6 (standard reference, not scraped)
- Carnegie Mellon 21-269, Riemann integration notes (standard reference, not scraped)
- J. Lebl, Basic Analysis I, Fundamental theorem of calculus (standard reference, not scraped)