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 ab, 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:=limxa+F(x)F(a),

which exists by One-sided limits of a monotone function always exist: for f nondecreasing on an interval I and cI, limxcf(x)=sup{f(x):xI, x<c} whenever I has points below c, limxc+f(x)=inf{f(x):xI, x>c} whenever it has points above c, and these satisfy limxcf(x)f(c)limxc+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{tS(F(t)F(t))  +  uT(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 FJF 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

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