Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05
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 a≤b, and let F:[a,b]→R be nondecreasing (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R, with the dictionary to monotone sequences). When a<b, write

βa:=lim⁡x→a+F(x)−F(a),

which exists by One-sided limits of a monotone function always exist: for f nondecreasing on an interval I and c∈I, lim⁡x→c−f(x)=sup⁡{f(x):x∈I, x<c} whenever I has points below c, lim⁡x→c+f(x)=inf⁡{f(x):x∈I, x>c} whenever it has points above c, and these satisfy lim⁡x→c−f(x)≤f(c)≤lim⁡x→c+f(x) and is nonnegative. When a=b, put βa:=0. For x∈[a,b] define the jump function JF by

JF(a):=0,

and, for x>a,

JF(x):=βa+sup⁡{∑t∈S(F(t)−F(t−))  +  ∑u∈T(F(u+)−F(u)):S⊆(a,x] finite,T⊆(a,x) finite}.

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 a<b, the endpoint defect at a is included separately because a nondecreasing function on [a,b] can fail to be continuous at the left endpoint without having a left-hand jump there. The convention βa=0 makes the degenerate interval [a,a] harmless.
  • The first sum collects left jumps at points at or before x, while the second collects right jumps at points strictly before x. Later A nondecreasing function splits uniquely into a jump part and a continuous part ↗ proves that these two contributions exactly remove the discontinuities of F, so F−JF is continuous.
  • If F is right-continuous, then every interior right jump is zero and the definition reduces to the usual cumulative left-jump function.

Depends on

Used by

Dependency tree · two levels

32 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