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 are outer regular and inner regular by compact sets
Statement
Let be nondecreasing and right-continuous, and let be the associated Lebesgue-Stieltjes measure. Then for every Borel set ,
If , then equivalently: for every there are an open set and a compact set with
Facts & Assumptions
Given: A nondecreasing right-continuous function , its Lebesgue-Stieltjes measure , a Borel set , and .
The half-open interval formulas hold for , including the formulas for open and closed intervals. (Interval formulas and atoms for a Lebesgue-Stieltjes measure)
Measures are continuous from below and from above. (Continuity from below for measures, Continuity from above when one set has finite measure)
The half-open intervals generate the Borel sigma-algebra on , 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)
Every closed bounded interval is compact. (Heine-Borel by bisection: every closed bounded interval is compact)
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
Every bounded half-open interval is regular. Let .
Choose so small that ; then the open interval contains and [L1] gives
Likewise choose with ; then the closed interval is compact by [L4], satisfies , and [L1] gives
[L1, L4, choose]
Fix and write . Let be the family of Borel subsets such that for every there is an open set with
By step 1.1, every trace with lies in . Those traces form an algebra on , because is an algebra on 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 . [step 1.1, L3, L5]
The family is a monotone class. If and , choose open with .
Then is open, contains , and
so . If instead , then has finite measure by [L1], so [L2] gives ; choose with , then choose open with . The open set contains , and
[step 2.1, L1, L2]
Step 3.1 makes a monotone class containing the algebra from step 2.1.
Therefore [L3] gives that every Borel subset of lies in : every bounded Borel set is relatively outer regular inside a compact interval. [step 2.1, step 3.1, L3]
Let be Borel. Apply step 4.1 to the Borel complement in the subspace .
Choose open with . Put . Then is closed in the compact interval , hence compact by [L4], and . Moreover
so . Thus every bounded Borel set is also inner regular by compact sets. [step 4.1, L4]
The global inner regularity follows by truncation. Put .
Then , so [L2] gives . For each , step 5.1 gives a compact with . Hence
while the reverse inequality is monotonicity. [step 5.1, L2, algebra]
For global outer regularity, first suppose . Choose so large that .
This is possible directly from [L2] on . Step 4.1 gives an open with . For each of the two tails and , decompose into unit half-open strips and apply step 4.1 on each compact strip, choosing the errors summably below ; enlarging each strip by a thin open shell whose -measure is also chosen summably below via [L1], the union of those stripwise open sets is open and contributes total excess below . Taking the union with gives an open set with . [step 4.1, step 6.1, L1, L2]
If , then every open also has by monotonicity.
So . 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
- The algebra of finite disjoint unions of half-open intervals in $\mathbb{R}$ with extended endpoints
- The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra
- Continuity from above when one set has finite measure
- Continuity from below for measures
- Heine-Borel by bisection: every closed bounded interval $[a,b]$ is compact
- Interval formulas and atoms for a Lebesgue-Stieltjes measure
- Assuming countable choice, finite-on-compacts Borel measures on $\mathbb{R}$ correspond to nondecreasing right-continuous functions modulo constants
- The monotone class generated by an algebra equals the sigma-algebra it generates
- Seven generating families for the Borel sigma-algebra on the real line
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
- Gerald B. Folland, Real Analysis, 2nd ed., Theorem 1.18 (standard reference, not scraped)