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 complex L^1 density defines a complex measure whose total variation is |h| dmu
Statement
Let be a measure space and let . Define Then is a complex measure on , and for every measurable ,
Facts & Assumptions
Given: A measure space and a function .
For an integrable function, the measurable-set integral is defined. (Integrable real and complex functions, and their integrals, Integral over a measurable subset)
Total variation is the supremum of the simple integrals against unit-bounded simple test functions. (Total variation is the supremum of simple integrals over unit-bounded test functions)
Every function admits dominated complex simple approximations. (Every L^1 function admits dominated complex simple approximations)
Arithmetic operations preserve measurability. (Closure properties of measurable functions used by the integral)
For a nonnegative measurable function , the set function is a measure. (The indefinite integral of a nonnegative measurable function is a measure)
The Lebesgue integral is complex-linear on . (The Lebesgue integral is linear on )
Proof
The set function is finite-valued because by [L1] and [L2]. If is a pairwise disjoint measurable sequence, then , so monotone convergence applied to the positive and negative parts of the real and imaginary parts of gives Thus is a complex measure.
Define Then and . By [L5], the function is measurable. Apply [L6] to and obtain a finite measure on . Applying [L4] to on gives complex simple functions with and For each , define the clipped simple function Then , and because one has Hence .
For any measurable and any countable measurable partition , the inequality in step 1.1 applied on each piece gives Taking the supremum over partitions shows .
Write the canonical representation of on as Because , each lies in . By the definition of and the linearity of the Lebesgue integral, Therefore So .
Since each is a unit-bounded complex simple function on , [L3] gives for every . Letting and using step 2.2 shows . Together with step 2.1, this proves .
Steps 1.1, 2.1, and 3.1 prove that is a complex measure and that its total variation is on every measurable set .
Depends on
A complex measure is a finite-valued countably additive set function
Integration against a signed or complex measure, and the class L^1(nu) = L^1(|nu|)
Total variation is the supremum of simple integrals over unit-bounded test functions
Integrals against signed or complex measures are bounded by total variation
Every L^1 function admits dominated complex simple approximations
Integral over a measurable subset
Monotone convergence for the integral
Closure properties of measurable functions used by the integral
Integrable real and complex functions, and their integrals
The modulus of an integral is bounded by the integral of the modulus
The indefinite integral of a nonnegative measurable function is a measure
The Lebesgue integral is linear on