Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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.

A nondecreasing function splits uniquely into a jump part and a continuous part

Statement

Let a≤b, let F:[a,b]→R be nondecreasing, and let JF be the jump function of The jump function of a nondecreasing function on a compact interval, and put

CF:=F−JF.

Then:

  1. JF and CF are nondecreasing;
  2. if a<b and (sn)n∈A is any enumeration without repetitions of the discontinuity set of F in (a,b), where A⊆N, then for every x>a, JF(x)=βa+∑n∈A, sn≤x(F(sn)−F(sn−))+∑n∈A, sn<x(F(sn+)−F(sn))+1{b}(x)(F(b)−F(b−));
  3. CF is continuous on [a,b];
  4. F=JF+CF on [a,b], and JF has exactly the same left and right jumps as F;
  5. when a<b, the endpoint defect at a, the interior left and right jump sizes, and the left jump at b determine JF pointwise, and then CF=F−JF is forced; when a=b, one has JF(a)=0 and CF(a)=F(a).

Facts & Assumptions

Given: Reals a≤b, the nondecreasing function F:[a,b]→R, the jump function JF, and the remainder CF=F−JF.

[A1]

The symbols are those of the statement.

Proof

technique · direct
1.1given

If a=b, the definition gives JF(a)=0 and CF(a)=F(a), so all five claims are immediate on the singleton interval. Hence assume a<b from now on.

1.2given

If a<x<y≤b, every finite pair (S,T) with S⊆(a,x] and T⊆(a,x) is also admissible for y, so JF(x)≤JF(y). The comparison with x=a follows from JF(a)=0 and the nonnegative definition of JF(y). Thus JF is nondecreasing on [a,b].

2.1step 1.2algebra

Fix a≤x<y≤b. First suppose x>a, and split any finite pair (S,T) admissible in the definition of JF(y) into its old part S0⊆(a,x], T0⊆(a,x) and its new part S1⊆(x,y], T1⊆[x,y). The old contribution, including βa, is at most JF(x). Order the distinct points of S1∪T1. Monotonicity of F makes the new jump contributions telescope through disjoint successive value intervals from F(x) to F(y); this includes the possible right jump F(x+)−F(x) when x∈T1, and gives a total at most F(y)−F(x). Taking the supremum over (S,T) yields JF(y)−JF(x)≤F(y)−F(x). If x=a, the endpoint contribution βa=F(a+)−F(a) followed by the jumps in (a,y] and (a,y) telescopes in the same way, giving more precisely 0≤JF(y)−βa≤F(y)−F(a+) and hence JF(y)≤F(y)−F(a). Therefore the increment inequality holds for every a≤x<y≤b, and CF(y)−CF(x)=F(y)−F(x)−(JF(y)−JF(x))≥0. Thus CF is nondecreasing, proving claim 1.

3.1step 2.1

By Froda's theorem: the set of discontinuities of a monotone function on an interval is at most countable, the injection into N being built from one fixed enumeration of the rationals by least index, so no choice principle is used, the discontinuity set of F in (a,b) is at most countable; index it without repetitions as (sn)n∈A for some A⊆N. At points outside that set both interior one-sided jump sizes vanish. The only remaining possible contribution in the defining supremum is the left jump at b, which occurs exactly when x=b. Thus The jump function of a nondecreasing function on a compact interval agrees with the nonnegative series JF(x)=βa+∑n∈A, sn≤x(F(sn)−F(sn−))+∑n∈A, sn<x(F(sn+)−F(sn))+1{b}(x)(F(b)−F(b−))(x>a). This is claim 2.

4.1step 2.1step 3.1

Fix c∈(a,b). Step 3.1 shows that JF(c)−JF(c−)=F(c)−F(c−),JF(c+)−JF(c)=F(c+)−F(c). Therefore CF(c)−CF(c−)=0,CF(c+)−CF(c)=0. Since CF is nondecreasing, 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) gives the one-sided limits at c, and the displayed equalities force CF(c−)=CF(c)=CF(c+). Hence CF is continuous at every interior point. Moreover, the displayed equalities show that JF has exactly the same left and right jumps as F. This proves claim 4 except for the tautological identity F=JF+CF.

4.2step 2.1step 3.1

To treat the endpoints, note first that step 2.1 with x=a gives 0≤JF(x)−βa≤F(x)−lim⁡t→a+F(t) for every x>a. Because the right-hand side tends to 0 as x↓a, JF(x)→βa. Hence CF(x)=F(x)−JF(x)⟶lim⁡x→a+F(x)−βa=F(a)=CF(a), so CF is right-continuous at a. At b, the endpoint term in step 3.1 gives JF(b)−JF(b−)=F(b)−F(b−), and therefore CF(b−)=CF(b). Thus CF is continuous on all of [a,b]. This proves claim 3.

5.1step 3.1step 4.2

Claim 4 contains the identity F=JF+CF by definition of CF. For claim 5, step 3.1 expresses JF(x) pointwise in terms of βa, the interior left and right jump sizes of F, and the left jump at b, so those data determine JF uniquely. Once JF is fixed, the remainder is forced by CF=F−JF.

6.1step 1.1step 1.2step 2.1step 3.1step 4.1step 4.2step 5.1∎

Steps 1.1 through 5.1 prove the theorem.

Depends on

Used by

Cited to discharge well-definedness by The jump function of a nondecreasing function on a compact interval.

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