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.
On a finite-measure space, a bounded functional on defines a finite signed measure
Statement
Let be a finite measure space, let , and let be a bounded linear functional. Define Then is a finite signed measure on .
Facts & Assumptions
Given: A finite measure space , an exponent , and a bounded linear functional .
A bounded linear functional on is linear and continuous with respect to the norm (A bounded linear functional on and its operator norm).
A real-valued countably additive set function with finite values is a signed measure (A signed measure is countably additive and takes at most one infinite value).
Dominated convergence applies to integrable majorants (Dominated convergence).
Proof
For every measurable , so and is a finite scalar. Also .
Let be pairwise disjoint measurable sets, and put Then pointwise and Because , the majorant is integrable, so [L3] gives
If are disjoint, then . By linearity of , So is finitely additive on disjoint measurable sets.
By continuity of from [L1], finite additivity from step 2.1, and the convergence from step 1.2, So is countably additive. Together with step 1.1, [L2] shows that is a finite signed measure.
Depends on
Used by
- On a finite-measure space, a bounded Lᵖ functional is integration against its Radon-Nikodym density Lemma
- The measure defined by a bounded Lᵖ functional is absolutely continuous with respect to μ Lemma
- On a sigma-finite measure space, every bounded linear functional on Lᵖ is integration against a unique L^q function Theorem
Dependency tree · two levels
16 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
- Gerald B. Folland, Real Analysis, 2nd ed., Theorem 6.15 (standard reference, not scraped)
- Richard F. Bass, Real Analysis for Graduate Students, Theorem 15.11 (standard reference, not scraped)
- John K. Hunter, Measure Theory, Theorem 7.14 (standard reference, not scraped)