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.
The Riemann integral of a bounded function over a bounded Jordan measurable set
Definition
Let be bounded in the metric sense of Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space and Jordan measurable, and let be bounded. Choose a nondegenerate rectangle , whose existence follows from Jordan inner and outer content and Jordan measurable bounded sets in , and define the zero extension The function is Riemann integrable over when is integrable over , and then Independence of the bounding rectangle, for both integrability and value, is proved in The Riemann integral over a Jordan set is independent of the bounding rectangle ↗ and recorded as the definition's forward justification. For , the zero extension is , so A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content gives .
Depends on
- Jordan inner and outer content and Jordan measurable bounded sets in $\mathbb{R}^m$
- A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content
- The lower and upper Darboux integrals over a nondegenerate rectangle in $\mathbb{R}^m$
- Axis-parallel rectangles in $\mathbb{R}^m$ and their volume
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space
- Lower bound, bounded below, bounded set
Used by
- Sections, lower and upper section integrals, and iterated Riemann integrals on product rectangles and Jordan sets Definition
- Finite Jordan covers bound upper integrals, while interior-disjoint Jordan subfamilies bound lower integrals Lemma
- The Riemann integral over a Jordan set is independent of the bounding rectangle Lemma
- Conventions and proved scope for the Riemann integral in ℝᵐ and Jordan content Remark
- A continuous real function on a compact Jordan measurable set is Riemann integrable over that set Theorem
- Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 84 results over 19 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. Lebl, Basic Analysis, Jordan Measurable Sets (standard reference, not scraped)
- J. Lebl, Basic Analysis, Outer Measure and Null Sets (standard reference, not scraped)