Alphabeta MathHow 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.
Henstock--Kurzweil and Lebesgue integral comparison on a compact interval
Statement
The compact-interval comparison is recorded in Henstock-Kurzweil versus Lebesgue: is Lebesgue integrable iff and are both HK integrable ‡: exactly when and are Henstock--Kurzweil integrable, and then the values of the two integrals of agree. The local HK notions and unconditional derivative FTC are The Henstock–Kurzweil integral on a compact interval, Every derivative is Henstock–Kurzweil integrable and satisfies Newton–Leibniz, and The indefinite Henstock–Kurzweil integral of a derivative is a primitive.
Remarks
Not proved here. The cited source supplies the comparison. In particular, it must not be inferred merely from the definition of Lebesgue integrability Integrable real and complex functions, and their integrals or from the unconditional HK theorem for derivatives.
Depends on
- Henstock-Kurzweil versus Lebesgue: $f$ is Lebesgue integrable iff $f$ and $|f|$ are both HK integrable
- The Henstock–Kurzweil integral on a compact interval
- Every derivative is Henstock–Kurzweil integrable and satisfies Newton–Leibniz
- The indefinite Henstock–Kurzweil integral of a derivative is a primitive
- Integrable real and complex functions, and their integrals
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
16 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
- Donald L. Cohn, Measure Theory, 2nd ed., Appendix H, Exercises 18, 20, and 22 (standard reference, not scraped)