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.
The total variation of a signed or complex measure is a positive measure
Statement
Let be a signed measure or a complex measure on . Then is a measure on .
Facts & Assumptions
Given: A signed measure or complex measure on .
The total variation is defined by a supremum of nonnegative partition sums over countable measurable partitions of . (The total variation |nu|(E) from countable measurable partitions)
A measure is a nonnegative set function with value at and countable additivity on pairwise disjoint measurable families. (Measures on sigma-algebras)
A finite family of nonempty sets has a choice function (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).
Proof
The set function is nonnegative by [L1]. Also , because every member of any countable measurable partition of is empty and its partition sum is .
Let be pairwise disjoint measurable sets and put . Fix and suppose for . For any , the definition of each supremum gives a countable partition of whose sum exceeds . Choose these finitely many partitions using [L3], enumerate all their cells in one countable partition, and append as one more cell. This is a countable measurable partition of , so [L1] gives . Let . If some , for each finite threshold choose one partition of that with sum above the threshold and append ; then . Hence in all cases for every , and taking the supremum of finite partial sums gives . No partitions were chosen across infinitely many .
Conversely, let be a countable measurable partition of . For each , countable additivity of on and the triangle inequality for finite partial sums and their limits give . For each , the cells partition , so by [L1]. Summing the first inequality over and interchanging two nonnegative series yields . Taking the supremum over all partitions gives .
Steps 1.2 and 1.3 prove countable additivity. Together with step 1.1 and [L2], this shows that is a measure.
Depends on
Measures on sigma-algebras
The total variation |nu|(E) from countable measurable partitions
Every natural-number-indexed list of nonempty sets has a choice function on its family of values
Every complex measure has finite total variation
For a signed measure, total variation is nu-plus plus nu-minus, finite partitions suffice, and nu-plus and nu-minus are extremal