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 jump function of a nondecreasing function on a compact interval
Definition
Let , and let be nondecreasing (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences). When , write
which exists by One-sided limits of a monotone function always exist: for nondecreasing on an interval and , whenever has points below , whenever it has points above , and these satisfy and is nonnegative. When , put . For define the jump function by
and, for ,
The summands are nonnegative, and the supremum is taken in the complete ordered field of the reals (Complete ordered field (least-upper-bound property)).
Remarks
- When , the endpoint defect at is included separately because a nondecreasing function on can fail to be continuous at the left endpoint without having a left-hand jump there. The convention makes the degenerate interval harmless.
- The first sum collects left jumps at points at or before , while the second collects right jumps at points strictly before . Later A nondecreasing function splits uniquely into a jump part and a continuous part ↗ proves that these two contributions exactly remove the discontinuities of , so is continuous.
- If is right-continuous, then every interior right jump is zero and the definition reduces to the usual cumulative left-jump function.
Depends on
- Lower bound, bounded below, bounded set
- Complete ordered field (least-upper-bound property)
- Finite sums and finite products, by recursion
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$, with the dictionary to monotone sequences
- The left and right limits of $f$ at $c$, as limits of the restrictions of $f$ to $A \cap (-\infty, c)$ and $A \cap (c, \infty)$
- One-sided limits of a monotone function always exist: for $f$ nondecreasing on an interval $I$ and $c \in I$, $\lim_{x \to c^{-}} f(x) = \sup\{f(x) : x \in I,\ x < c\}$ whenever $I$ has points below $c$, $\lim_{x \to c^{+}} f(x) = \inf\{f(x) : x \in I,\ x > c\}$ whenever it has points above $c$, and these satisfy $\lim_{x \to c^{-}} f(x) \le f(c) \le \lim_{x \to c^{+}} f(x)$
Used by
Dependency tree · two levels
29 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
- A. M. Bruckner, J. B. Bruckner, and B. S. Thomson, Real Analysis, 2nd ed., Chapter 7 (standard reference, not scraped)