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.
has an unbounded derivative whose Henstock–Kurzweil integral is
Example
Define and for . Then is differentiable on and
has an unbounded derivative whose Henstock–Kurzweil integral is .
The derivative of is Henstock–Kurzweil integrable on .
Facts & Assumptions
Given: The displayed function and its derivative candidate .
If , is differentiable in the domain-relative sense, including at the endpoints, and , then is Henstock–Kurzweil integrable and (Every derivative is Henstock–Kurzweil integrable and satisfies Newton–Leibniz).
For every integer , , , and (Quarter-turn values and shifts by pi/2 and pi, The zero sets of sine and cosine and the least positive common period 2 pi).
If is differentiable at and is differentiable at , then the chain rule gives (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with ).
The product rule holds for differentiable real functions, and the quotient rule holds where the denominator is nonzero (Sums, scalar multiples, products and quotients: , , , and when ).
Sine and cosine have derivatives and (The derivatives of sine and cosine are cosine and minus sine).
For every real , (Parity and the Pythagorean identity for sine and cosine).
Verification
Applying [L3], [L4], and [L5] gives the displayed derivative for , while [L6] gives and hence . For every natural , at the values in [L2] give , which is unbounded.
Applying [L1] gives HK integrability and .
Depends on
- Every derivative is Henstock–Kurzweil integrable and satisfies Newton–Leibniz
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- 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$
- The derivatives of sine and cosine are cosine and minus sine
- Quarter-turn values and shifts by pi/2 and pi
- The zero sets of sine and cosine and the least positive common period 2 pi
- Parity and the Pythagorean identity for sine and cosine
Used by
- Henstock–Kurzweil integrability does not imply integrability of the absolute value Counterexample
- False: every derivative is Riemann integrable False statement
- False: every Henstock–Kurzweil integrable function is bounded False statement
Dependency tree · two levels
35 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
- Alessandro Fonda, The Kurzweil-Henstock Integral for Undergraduates, Ch. 1 (standard reference, not scraped)
- Andrew Bruckner, Judith Bruckner and Brian Thomson, Real Analysis, Section 1.21 (standard reference, not scraped)