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.
The Riemann–Stieltjes integral is unique
Statement
For fixed , at most one real number satisfies the mesh-limit condition defining .
Facts & Assumptions
Given: Two reals satisfying the defining mesh condition for the same functions .
The mesh-limit condition quantifies over every sufficiently fine tagged partition (Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral).
Uniform partitions have mesh for every natural (Partition of as a finite strictly increasing list , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions, The canonical natural of a field).
Reciprocal naturals become arbitrarily small (For every in a complete ordered field there is a natural with ).
and exactly when (The triangle inequality, Basic properties of the absolute value).
Proof
Given , choose positive thresholds for error in the two mesh conditions. By [L3] choose a natural whose uniform partition has mesh smaller than both thresholds, and give it arbitrary tags.
For its sum , . Since this holds for every , and . The singleton interval has only the prescribed value .
Depends on
- Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral
- Partition of $[a,b]$ as a finite strictly increasing list $a = t_0 < t_1 < \dots < t_n = b$, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- The triangle inequality
- Basic properties of the absolute value
Used by
- The total-variation bound for a Riemann–Stieltjes integral Corollary
- A common jump can destroy Riemann–Stieltjes integrability Counterexample
- A continuous integrand is Riemann–Stieltjes integrable against every bounded-variation integrator Theorem
- Change of variable for the Riemann–Stieltjes integral Theorem
- Linearity and interval additivity of the Riemann–Stieltjes integral Theorem
- Riemann–Stieltjes integration by parts Theorem
- Young's Riemann–Stieltjes existence theorem for rational Hölder exponents Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 54 results over 13 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
- William F. Trench, Introduction to Real Analysis, Definition 3.1.5 (standard reference, not scraped)