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.
Lusin's theorem for a Radon measure
Statement
Let be a Radon measure on an LCH space in the convention of Radon measure on an LCH space. Let be Borel with and let be Borel measurable. For every there is compact such that and is continuous.
Facts & Assumptions
Given: as in the Statement and .
Radon means finite on compact sets, outer regular on Borel sets, and compact-inner-regular on open sets (Radon measure on an LCH space). We do not assume the stronger all-Borel convention of Regular Borel measure on an LCH space.
Proof
First let be Borel of finite measure and let . By [L1], choose open of finite measure and compact with . By outer regularity choose open with . Then is compact and contained in . Since is disjoint from , , and hence . This proves compact approximation for each finite-measure Borel set using only [L1].
Since is complex-valued and , continuity from above gives an for which satisfies . For each , partition the disk into finitely many nonempty disjoint Borel cells , , each of diameter less than . Such cells can be obtained by intersecting the disk with a finite half-open square grid. Their preimages partition into finite-measure Borel sets.
Apply step 1.1 to choose compact with . Put and . Each is compact and thus closed in ; their intersection is a closed subset of the compact , hence compact. Moreover and .
For each , the finitely many disjoint compact sets cover . Each is relatively clopen, because its complement is a finite union of closed sets. On it, the values of lie in and have oscillation below . Given and a positive tolerance, choose so is smaller; its clopen cell piece is a neighbourhood witnessing continuity at . The empty case is vacuous. Thus is continuous.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
10 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
- Donald L. Cohn, Measure Theory, 2nd ed., Chapter 7 (standard reference, not scraped)