ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-08-11

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.

A finite-step integrator gives a weighted sum over its jumps

Example

Let $a < b$ , let $c_{1} < \dots < c_{m}$ be points of the open interval $(a, b)$ , as in the one-jump example, and let $α = C + \sum_{j = 1}^{m} w_{j} H_{c_{j}} .$ For every continuous $f$ , $\int_{a}^{b} f d α = \sum_{j = 1}^{m} w_{j} f (c_{j}) .$

Facts & Assumptions

Given: The displayed finite-step integrator and a continuous $f$ .

[L1]

For $a < c < b$ and $H_{c}$ equal to $0$ below $c$ and $1$ from $c$ on, every continuous $f$ has $\int_{a}^{b} f d H_{c} = f (c)$ : a single jump of weight one at an interior point evaluates $f$ there (A one-jump integrator evaluates a continuous integrand at the jump).

[L2]

The Stieltjes integral is linear in its integrator (Linearity and interval additivity of the Riemann–Stieltjes integral).

Verification

technique · computation

1.1

The constant term has every increment equal to zero. By [L1], each $H_{c_{j}}$ contributes $f (c_{j})$ , and finite linearity [L2] gives the displayed sum.

L1L2

2.1

Ordering the distinct jump points prevents double counting. The jump points are interior because [L1] places them strictly inside, and the restriction is not cosmetic: $H_{a}$ takes the value $1$ at every point of $[a, b]$ , so a jump placed at $a$ makes every increment zero and contributes nothing, while the weighted sum would still count $w f (a)$ .

L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

W. Rudin, Principles of Mathematical Analysis, Ch. 6, Theorem 6.15 (standard reference, not scraped)