Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-07
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 E be Borel with μ(E)< and let f:EC be Borel measurable. For every ε>0 there is compact KE such that μ(EK)<ε and fK is continuous.

Facts & Assumptions

Given: X,μ,E,f as in the Statement and ε>0.

[L1]

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

technique · derive compact approximation for finite-measure sets, then intersect finite compact cell cores
1.1

First let B be Borel of finite measure and let δ>0. By [L1], choose open UB of finite measure and compact LU with μ(UL)<δ/2. By outer regularity choose open OUB with μ(O)<μ(UB)+δ/2. Then H=LO is compact and contained in B. Since B is disjoint from UB, μ(BO)<δ/2, and hence μ(BH)μ(UL)+μ(BO)<δ. This proves compact approximation for each finite-measure Borel set using only [L1].

L1givenconstruct
1.2

Since f is complex-valued and μ(E)<, continuity from above gives an M>0 for which B={xE:f(x)M} satisfies μ(EB)<ε/4. For each m0, partition the disk zM into finitely many nonempty disjoint Borel cells Cm,j, 1jJm, each of diameter less than 2m. Such cells can be obtained by intersecting the disk with a finite half-open square grid. Their preimages Bm,j partition B into finite-measure Borel sets.

givenconstruct
2.1

Apply step 1.1 to choose compact Hm,jBm,j with μ(Bm,jHm,j)<ε2m3/Jm. Put Hm=j=1JmHm,j and K=m0Hm. Each Hm is compact and thus closed in X; their intersection is a closed subset of the compact H0, hence compact. Moreover KBE and μ(EK)μ(EB)+m0μ(BHm)<ε/4+m0ε2m3=ε/2<ε.

step 1.1step 1.2construct
3.1

For each m, the finitely many disjoint compact sets KHm,j cover K. Each is relatively clopen, because its complement is a finite union of closed sets. On it, the values of f lie in Cm,j and have oscillation below 2m. Given xK and a positive tolerance, choose m so 2m is smaller; its clopen cell piece is a neighbourhood witnessing continuity at x. The empty K case is vacuous. Thus fK is continuous.

step 2.1

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