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.
A function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra
Statement
Assume the Axiom of Countable Choice. Let be a measure space and let be its completion. If is measurable with respect to , then there is an -measurable function such that almost everywhere.
Facts & Assumptions
Given: The Axiom of Countable Choice, a measure space , its completion , and an -measurable function .
Every measurable function admits simple approximations dominated by its absolute value. (Every measurable function admits simple approximations dominated by its absolute value)
A completed measurable set has the form with and contained in a measurable null set. (The completion domain and proposed completed set function of a measure space)
Assuming Countable Choice, the completion is a complete measure space extending the original measure, and countable unions of completed null sets are completed null sets. (Assuming countable choice, every measure space has a unique complete extension to its completion, Null sets are closed under countable unions and, in a complete space, under arbitrary subsets)
Pointwise limsup of a sequence of measurable functions is measurable. (Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable)
Proof
By [L1], choose simple -measurable functions [L1, choose] with and for every . Write the canonical representation of as where the are pairwise disjoint completed measurable level sets.
For each pair , apply [L2] to and choose [L2, L3, choose] together with a completed null set such that with . Because , the sets remain pairwise disjoint. Define Then each is -measurable and simple. Let . By [L3], is a completed measurable null set, and for every one has for all .
Define [step 1.1, step 1.2, L4] By [L4], the function is -measurable. If , then step 1.2 gives for every , and step 1.1 gives , so . Hence on .
The null set is measurable in the completion by [L3], so step 2.1 says [step 2.1, L3] exactly that almost everywhere. Since is -measurable, it is the required base-measurable representative.
Depends on
Every measurable function admits simple approximations dominated by its absolute value
The completion domain and proposed completed set function of a measure space
Null sets are closed under countable unions and, in a complete space, under arbitrary subsets
Assuming countable choice, every measure space has a unique complete extension to its completion
Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable