Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27
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.

Lebesgue-Stieltjes measures on R are outer regular and inner regular by compact sets

Statement

Let F:RR be nondecreasing and right-continuous, and let μF be the associated Lebesgue-Stieltjes measure. Then for every Borel set ER,

μF(E)=inf{μF(U):EU, U open}=sup{μF(K):KE, K compact}.

If μF(E)<+, then equivalently: for every ε>0 there are an open set U and a compact set K with

KEU,μF(UE)<ε,μF(EK)<ε.

Facts & Assumptions

Given: A nondecreasing right-continuous function F:RR, its Lebesgue-Stieltjes measure μF, a Borel set ER, and ε>0.

[L1]

The half-open interval formulas hold for μF, including the formulas for open and closed intervals. (Interval formulas and atoms for a Lebesgue-Stieltjes measure)

[L2]
[L3]

The half-open intervals generate the Borel sigma-algebra on R, and the monotone class generated by an algebra is the sigma-algebra it generates. (Seven generating families for the Borel sigma-algebra on the real line, The monotone class generated by an algebra equals the sigma-algebra it generates)

[L5]

The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra. (The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra)

Proof

technique · direct
1.1

Every bounded half-open interval is regular. Let I=(a,b].

L1L4choose

Choose η>0 so small that F((b+η))F(b)<ε; then the open interval U:=(a,b+η) contains I and [L1] gives

μF(UI)=μF((b,b+η))<ε.

Likewise choose δ>0 with F((a+δ))F(a)<ε; then the closed interval K:=[a+δ,b] is compact by [L4], satisfies KI, and [L1] gives

μF(IK)=μF((a,a+δ))=F((a+δ))F(a)<ε.

[L1, L4, choose]

2.1

Fix m1 and write Im:=[m,m]. Let Om be the family of Borel subsets AIm such that for every ε>0 there is an open set UR with

step 1.1L3L5

AU,μF((UIm)A)<ε.

By step 1.1, every trace HIm with HH lies in Om. Those traces form an algebra on Im, because H is an algebra on R and traces preserve complements and finite unions. By [L5] together with the generator statement of [L3], they generate the Borel sigma-algebra of the subspace Im. [step 1.1, L3, L5]

3.1

The family Om is a monotone class. If AnA and AnOm, choose open UnAn with μF((UnIm)An)<ε2n1.

step 2.1L1L2

Then U:=nUn is open, contains A, and

(UIm)An((UnIm)An),

so μF((UIm)A)<ε. If instead AnA, then A0Im has finite measure by [L1], so [L2] gives μF(AnA)0; choose n with μF(AnA)<ε/2, then choose open UnAn with μF((UnIm)An)<ε/2. The open set Un contains A, and

μF((UnIm)A)μF((UnIm)An)+μF(AnA)<ε.

[step 2.1, L1, L2]

4.1

Step 3.1 makes Om a monotone class containing the algebra from step 2.1.

step 2.1step 3.1L3

Therefore [L3] gives that every Borel subset of Im lies in Om: every bounded Borel set is relatively outer regular inside a compact interval. [step 2.1, step 3.1, L3]

5.1

Let AIm be Borel. Apply step 4.1 to the Borel complement ImA in the subspace Im.

step 4.1L4

Choose open UImA with μF((UIm)(ImA))<ε. Put K:=ImU. Then K is closed in the compact interval Im, hence compact by [L4], and KA. Moreover

AK=AU=(UIm)(ImA),

so μF(AK)<ε. Thus every bounded Borel set is also inner regular by compact sets. [step 4.1, L4]

6.1

The global inner regularity follows by truncation. Put Em:=EIm.

step 5.1L2algebra

Then EmE, so [L2] gives μF(E)=supmμF(Em). For each m, step 5.1 gives a compact KmEmE with μF(EmKm)<1/(m+1). Hence

sup{μF(K):KE, K compact}supmμF(Km)=supmμF(Em)=μF(E),

while the reverse inequality is monotonicity. [step 5.1, L2, algebra]

7.1

For global outer regularity, first suppose μF(E)<+. Choose m so large that μF(EIm)<ε/3.

step 4.1step 6.1L1L2

This is possible directly from [L2] on EImE. Step 4.1 gives an open VEIm with μF((VIm)E)<ε/3. For each of the two tails E(m,) and E(,m), decompose into unit half-open strips and apply step 4.1 on each compact strip, choosing the errors summably below ε/3; enlarging each strip by a thin open shell whose μF-measure is also chosen summably below ε/3 via [L1], the union of those stripwise open sets is open and contributes total excess below 2ε/3. Taking the union with V gives an open set UE with μF(UE)<ε. [step 4.1, step 6.1, L1, L2]

8.1

If μF(E)=+, then every open UE also has μF(U)=+ by monotonicity.

step 6.1step 7.1algebra

So inf{μF(U):EU, U open}=+=μF(E). Combining this with step 7.1 gives the outer regularity equality in all cases. The inner regularity equality is step 6.1, and the finite-measure ε-approximation statement is exactly the combination of steps 6.1 and 7.1. [step 6.1, step 7.1, algebra] ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 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