Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)
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.

Assuming countable choice, finite-on-compacts Borel measures on R correspond to nondecreasing right-continuous functions modulo constants

Statement

Assume the Axiom of Countable Choice. Let μ be a Borel measure on R finite on compact sets, and let Fμ be its normalized distribution function from The distribution function of a Borel measure on R, normalized at 0. Then:

  1. Fμ is nondecreasing and right-continuous;

  2. for every a<b,

    Fμ(b)−Fμ(a)=μ((a,b]);

  3. the Lebesgue-Stieltjes measure attached to Fμ is exactly μ.

Conversely, if F,G:R→R are nondecreasing and right-continuous, then μF=μG if and only if F−G is constant on R.

Facts & Assumptions

Given: Countable choice, a Borel measure μ on R finite on compact sets, its distribution function Fμ, and two nondecreasing right-continuous functions F,G:R→R.

[L1]

Measures are continuous from above when one set in the decreasing chain has finite measure. (Continuity from above when one set has finite measure)

[L3]

Assuming countable choice (The Axiom of Countable Choice (ACω)), every nondecreasing right-continuous function defines a Borel measure on R with the prescribed values on half-open intervals (Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on R). This is where the stated choice assumption is used.

[L4]

A Borel measure finite on compact sets is uniquely determined by its values on half-open intervals (a,b]. (The interval data on (a,b] determines the Borel measure uniquely)

Proof

technique · direct
1.1givenalgebra

The function Fμ is nondecreasing.

If 0≤x<y, then (0,x]⊆(0,y], so Fμ(x)≤Fμ(y). If x<y≤0, then (y,0]⊆(x,0], so −μ((x,0])≤−μ((y,0]), again giving Fμ(x)≤Fμ(y). If x<0≤y, then Fμ(y)−Fμ(x)=μ((0,y])+μ((x,0])=μ((x,y])≥0. [given, algebra]

1.2L3algebra

Suppose first that μF=μG. Then for every a<b,

0=μF((a,b])−μG((a,b])=(F(b)−G(b))−(F(a)−G(a)).

So F(b)−G(b)=F(a)−G(a) for all a<b, and therefore F−G is constant. [algebra]

1.3algebra

Conversely, if F−G is constant, then F(b)−F(a)=G(b)−G(a) for every a<b.

2.1step 1.1givenalgebra

For every a<b one has Fμ(b)−Fμ(a)=μ((a,b]).

In the three sign cases:

μ((0,b])−μ((0,a])=μ((a,b])(0≤a<b),

−μ((b,0])+μ((a,0])=μ((a,b])(a<b≤0),

and

μ((0,b])+μ((a,0])=μ((a,b])(a<0≤b).

So the displayed interval formula always holds. [step 1.1, given, algebra]

3.1step 2.1L1

The function Fμ is right-continuous. Fix x∈R and let hn↓0 with hn>0.

For all large n one has x+hn<0 when x<0, while for x≥0 no sign change occurs. In either case, step 2.1 gives

Fμ(x+hn)−Fμ(x)=μ((x,x+hn]).

The sets (x,x+hn] decrease to ∅, and the first one has finite measure because it is contained in a compact interval. Therefore [L1] gives μ((x,x+hn])→0, so Fμ(x+hn)→Fμ(x). [step 2.1, L1]

4.1step 2.1step 3.1L3

By [L3], the function Fμ determines a Lebesgue-Stieltjes measure μFμ.

Step 2.1 says that μFμ and μ agree on every half-open interval, so [L4] gives μFμ=μ. [step 2.1, step 3.1, L3, L4]

The interval values of μF and μG therefore agree by [L3], and [L4] yields μF=μG. Together with steps 1.1, 1.2, 1.3, 2.1, and 3.1 this proves the theorem. [step 1.1, step 1.2, step 1.3, step 2.1, step 3.1, L3, L4] ∎

Depends on

Used by

Dependency tree · two levels

23 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