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.

✓ 9 results · all verified · 5 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Lebesgue-Stieltjes Measures and Distribution Functions - Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The identity function generates Lebesgue measure

Example

Assuming the Axiom of Countable Choice, for $F (x) = x$ the associated Lebesgue-Stieltjes measure is exactly Lebesgue measure. In particular, the interval formulas become the ordinary length formulas

$λ ((a, b]) = b - a, λ ((a, b)) = b - a, λ ([a, b]) = b - a .$

Facts & Assumptions

Given: The Axiom of Countable Choice and the identity function $F (x) = x$ on $R$ .

[L1]

Assuming Countable Choice, the Lebesgue-Stieltjes measure of the identity function is Lebesgue measure. (Lebesgue measure is the Lebesgue-Stieltjes measure of the identity function)

[L2]

The interval formulas for a Lebesgue-Stieltjes measure recover open, closed, and half-open interval values from the distribution function. (Interval formulas and atoms for a Lebesgue-Stieltjes measure)

Verification

technique · direct

1.1L1

By [L1], the measure attached to $F (x) = x$ is $λ$ .

2.1step 1.1L2∎

Applying [L2] with $F (x) = x$ gives [step 1.1, L2] $F (b) - F (a) = F (b^{-}) - F (a) = F (b) - F (a^{-}) = b - a$ , so every one of the four interval conventions has measure $b - a$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A single jump generates the Dirac mass at $0$

Example

Let

$F (x) : = {\begin{cases} 0, & x < 0, \\ 1, & x \geq 0. \end{cases}$

Then the associated Lebesgue-Stieltjes measure is the Dirac mass at $0$ .

Facts & Assumptions

Given: The step function $F$ displayed above and its Lebesgue-Stieltjes measure $μ_{F}$ .

[L1]

Lebesgue-Stieltjes singleton masses are jumps, and half-open interval values are increments. (Interval formulas and atoms for a Lebesgue-Stieltjes measure)

Verification

technique · direct

1.1givenL1

The only jump of $F$ occurs at $0$ , where $F (0) - F (0^{-}) = 1$ , so [L1] gives $μ_{F} ({0}) = 1$ .

2.1step 1.1L1∎

If $x \neq 0$ , then $F (x) = F (x^{-})$ , so [L1] gives $μ_{F} ({x}) = 0$ ; and for any interval $(a, b]$ , the increment $F (b) - F (a)$ is $1$ exactly when $a < 0 \leq b$ and is $0$ otherwise, which is exactly the interval behavior of $δ_{0}$ .

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A step function generates a finite atomic measure

Example

Fix numbers $x_{1} < \dots < x_{m}$ and positive masses $α_{1}, \dots, α_{m}$ , and define

$F (x) : = \sum_{x_{j} \leq x} α_{j} .$

Then the Lebesgue-Stieltjes measure of $F$ is the finite atomic measure

$μ_{F} = \sum_{j = 1}^{m} α_{j} δ_{x_{j}} .$

Facts & Assumptions

Given: Points $x_{1} < \dots < x_{m}$ , positive numbers $α_{1}, \dots, α_{m}$ , the step function $F (x) = \sum_{x_{j} \leq x} α_{j}$ , and its Lebesgue-Stieltjes measure $μ_{F}$ .

[L1]

Finite weighted sums of Dirac measures are measures. (A Dirac set function is a probability measure, Nonnegative scalar multiples and countable weighted sums of measures are measures)

[L2]

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

Verification

technique · direct

1.1L1

Let $ν : = \sum_{j = 1}^{m} α_{j} δ_{x_{j}}$ . By [L1], this is a Borel measure on $R$ .

2.1givenstep 1.1algebra

For every $a < b$ ,

$ν ((a, b]) = \sum_{a < x_{j} \leq b} α_{j} .$

On the other hand, because $F (x) = \sum_{x_{j} \leq x} α_{j}$ , one has

$F (b) - F (a) = \sum_{x_{j} \leq b} α_{j} - \sum_{x_{j} \leq a} α_{j} = \sum_{a < x_{j} \leq b} α_{j} = ν ((a, b]) .$

So $μ_{F}$ and $ν$ agree on every half-open interval $(a, b]$ . [given, step 1.1, algebra]

3.1step 2.1L2∎

Both $μ_{F}$ and $ν$ are Borel measures on $R$ finite on [step 2.1, L2] compact sets. By step 2.1 and [L2], they are equal on every Borel set. Thus $μ_{F} = \sum_{j = 1}^{m} α_{j} δ_{x_{j}}$ , which is the claimed formula.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Two different normalizations give the same Lebesgue-Stieltjes measure

Example

If $G (x) = F (x) + 3$ , then $F$ and $G$ define the same Lebesgue-Stieltjes measure. This is the additive-constant ambiguity that the normalization $F_{μ} (0) = 0$ removes.

Facts & Assumptions

Given: Countable choice, a nondecreasing right-continuous function $F : R \to R$ , and the shifted function $G : = F + 3$ .

[L1]

Assuming countable choice, two nondecreasing right-continuous functions define the same Lebesgue-Stieltjes measure exactly when their difference is constant. (Assuming countable choice, finite-on-compacts Borel measures on $R$ correspond to nondecreasing right-continuous functions modulo constants)

Verification

technique · direct

1.1given

The function $G$ is nondecreasing and right-continuous whenever $F$ is, and [given] $G - F$ is the constant function $3$ .

2.1step 1.1L1∎

Therefore [L1] gives $μ_{G} = μ_{F}$ . The two distribution functions are [step 1.1, L1] distinct unless $3 = 0$ , so the normalization convention is doing real work.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The interval formulas for a function with one jump

Example

For the step function

$F (x) : = {\begin{cases} 0, & x < 0, \\ 1, & x \geq 0, \end{cases}$

the four interval conventions visibly differ at the jump:

$μ_{F} ((- 1, 0)) = 0, μ_{F} ((- 1, 0]) = 1, μ_{F} ([0, 1)) = 1, μ_{F} ((0, 1]) = 0.$

Facts & Assumptions

Given: The step function $F$ above and its Lebesgue-Stieltjes measure $μ_{F}$ .

[L1]

For a Lebesgue-Stieltjes measure, the open, closed, and half-open interval formulas are $μ_{F} ((a, b)) = F (b^{-}) - F (a)$ , $μ_{F} ((a, b]) = F (b) - F (a)$ , $μ_{F} ([a, b)) = F (b^{-}) - F (a^{-})$ , and $μ_{F} ([a, b]) = F (b) - F (a^{-})$ . (Interval formulas and atoms for a Lebesgue-Stieltjes measure)

Verification

technique · direct

1.1given

For this $F$ , one has [given] $F (- 1) = F (- 1^{-}) = 0$ , $F (0^{-}) = 0$ , $F (0) = 1$ , $F (1^{-}) = 1$ , and $F (1) = 1$ .

2.1step 1.1L1∎

Substituting those values into [L1] gives [step 1.1, L1] $μ_{F} ((- 1, 0)) = 0 - 0 = 0$ , $μ_{F} ((- 1, 0]) = 1 - 0 = 1$ , $μ_{F} ([0, 1)) = 1 - 0 = 1$ , and $μ_{F} ((0, 1]) = 1 - 1 = 0$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The Cantor measure is concentrated on the Cantor set

Example

The Cantor measure $μ_{c}$ is a probability measure with

$μ_{c} (C) = 1, μ_{c} (R ∖ C) = 0.$

So it is entirely supported on the Cantor set even though the Cantor set has Lebesgue measure $0$ .

Facts & Assumptions

Given: The Cantor measure $μ_{c}$ and the Cantor set $C$ .

[L1]

The Cantor measure is a singular atomless probability measure concentrated on the Cantor set. (The Cantor measure is a singular atomless probability measure concentrated on the Cantor set)

Verification

technique · direct

1.1L1

By [L1], $μ_{c} (R ∖ C) = 0$ .

2.1step 1.1L1∎

The same fact [L1] says $μ_{c} ([0, 1]) = 1$ , hence [step 1.1, L1] $μ_{c} (C) = 1 - μ_{c} ([0, 1] ∖ C) = 1$ . This is exactly what concentration on $C$ means.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-27Open item page →

The arctangent distribution function generates a Borel probability measure

Example

Assume the Axiom of Countable Choice and let

$F (x) : = \frac{\arctan (x)}{π} + \frac{1}{2} .$

Then $F$ is increasing and continuous, so it defines a Lebesgue-Stieltjes measure $μ_{F}$ . Its half-open interval values are

$μ_{F} ((a, b]) = \frac{\arctan (b) - \arctan (a)}{π},$

and $μ_{F}$ is a probability measure.

Facts & Assumptions

Given: The Axiom of Countable Choice, the function $F (x) = \arctan (x) / π + 1 / 2$ , and its Lebesgue-Stieltjes measure $μ_{F}$ .

[L1]

Assuming Countable Choice, every increasing right-continuous function defines a Lebesgue-Stieltjes measure, with half-open interval values given by increments. (Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on $R$ )

[L2]

Measures are continuous from below along increasing sets. (Continuity from below for measures)

Verification

technique · direct

1.1givenL1

The function $F$ is increasing and continuous, hence right-continuous, so [L1] gives a measure $μ_{F}$ with the following interval values.

$μ_{F} ((a, b]) = F (b) - F (a) = \frac{\arctan (b) - \arctan (a)}{π} .$

2.1step 1.1L2

The intervals $(- n - 1, n + 1]$ increase to $R$ .

$μ_{F} ((- n - 1, n + 1]) = F (n + 1) - F (- n - 1) = \frac{2 \arctan (n + 1)}{π} .$

Because $\arctan (n + 1) \to π / 2$ , [L2] gives $μ_{F} (R) = \lim_{n} 2 \arctan (n + 1) / π = 1$ . So $μ_{F}$ is a probability measure. [step 1.1, L2] ∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

A nondecreasing function that is not right-continuous can fail countable additivity

Statement refuted

That the interval prescription $μ ((a, b]) = F (b) - F (a)$ still defines a countably additive Borel measure when $F$ is merely nondecreasing and not right-continuous.

Facts & Assumptions

Given: The nondecreasing function

$F (x) : = {\begin{cases} 0, & x \leq 0, \\ 1, & x > 0. \end{cases}$

[L1]

Measures are continuous from above on decreasing sets when the first set has finite measure. (Continuity from above when one set has finite measure)

Counterexample

technique · direct

1.1given

If a Borel measure $μ$ satisfied $μ ((a, b]) = F (b) - F (a)$ , then [given] $μ ((0, 1 / n]) = 1$ for every $n$ , because $F (1 / n) = 1$ and $F (0) = 0$ .

2.1step 1.1L1∎

The sets $(0, 1 / n]$ decrease to $\emptyset$ , and [step 1.1, L1] $μ ((0, 1]) = 1 < + \infty$ . Therefore [L1] would force $μ ((0, 1 / n]) \to μ (\emptyset) = 0$ , contradicting step 1.1. So the interval prescription fails countable additivity for this nondecreasing non-right-continuous $F$ .

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-27Open item page →

The Cantor measure is atomless but not absolutely continuous with respect to Lebesgue measure

Statement refuted

That every atomless Borel measure on $R$ must be absolutely continuous with respect to Lebesgue measure.

Facts & Assumptions

Given: The Axiom of Countable Choice and the Cantor measure $μ_{c}$ .

[L1]

Assuming Countable Choice, the Cantor measure is an atomless probability measure singular with respect to Lebesgue measure. (The Cantor measure is a singular atomless probability measure concentrated on the Cantor set)

Counterexample

technique · direct

1.1L1

By [L1], the measure $μ_{c}$ is atomless.

2.1step 1.1L1∎

The same fact [L1] says that $μ_{c}$ is singular and has total mass $1$ . [step 1.1, L1] If it were also absolutely continuous with respect to Lebesgue measure, its concentration on a Lebesgue-null set would force its total mass to be $0$ , a contradiction. Therefore atomlessness does not imply absolute continuity.

Lebesgue-Stieltjes Measures and Distribution Functions - Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The identity function generates Lebesgue measure

Example

Facts & Assumptions

Verification

A single jump generates the Dirac mass at 00

Example

Facts & Assumptions

Verification

A step function generates a finite atomic measure

Example

Facts & Assumptions

Verification

Two different normalizations give the same Lebesgue-Stieltjes measure

Example

Facts & Assumptions

Verification

The interval formulas for a function with one jump

Example

Facts & Assumptions

Verification

The Cantor measure is concentrated on the Cantor set

Example

Facts & Assumptions

Verification

The arctangent distribution function generates a Borel probability measure

Example

Facts & Assumptions

Verification

A nondecreasing function that is not right-continuous can fail countable additivity

Statement refuted

Facts & Assumptions

Counterexample

The Cantor measure is atomless but not absolutely continuous with respect to Lebesgue measure

Statement refuted

Facts & Assumptions

Counterexample

Sources

A single jump generates the Dirac mass at $0$