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.
Differentiation under the integral sign
Statement
Let be an open interval and let be such that:
- for every , the function is integrable;
- for almost every , the map is differentiable on ;
- for every , the function extended by zero where the derivative is undefined, is measurable;
- there are a measurable null set and a nonnegative measurable function with and for every and every .
Then is differentiable on , and with the same zero extension in the last integral.
Facts & Assumptions
Given: An open interval , a function satisfying the first three displayed hypotheses, and a measurable null set together with a nonnegative measurable majorant satisfying hypothesis 4. Choose a measurable null set outside which hypothesis 2 holds, and put .
Dominated convergence applies to integrable complex-valued functions under a single majorant (Dominated convergence).
The mean value theorem bounds difference quotients by a derivative bound on an interval (The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with ).
The complex integral is linear on (The Lebesgue integral is linear on ).
The rationals are dense in the reals (The rationals embed densely in the reals).
Proof
Fix and let with and . Define For every , differentiability in gives . Give the derivative value zero on ; this measurable modification differs from the stated zero extension only on a null set, so it has the same integral.
For each , hypothesis 1 makes and integrable and therefore measurable, so is measurable. Fix and . If , then is immediate. Otherwise put so and Apply [L2] to the real-valued function on the segment joining to . For some interior point of that segment, Hypothesis 3 and the zero extension make the limit measurable. Therefore [L1] applies to .
By [L1], Linearity of the integral gives This holds for every supplied sequence of admissible nonzero increments.
The same mean-value estimate as in step 2.1, with any in place of , gives outside . Integrating yields , so is continuous. Consequently is continuous on the punctured interval of admissible increments. If failed to tend to as , there would be an and, for every , a nonzero admissible with and . Continuity of and [L4] give a rational admissible with and . Fix an enumeration of and take the first such rational for each ; this is a definable selection from a countable set and uses no Countable Choice. Then , contradicting step 3.1. Thus , which is precisely . Since was arbitrary, the theorem follows.