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.
Complex l one functionals on finite measure spaces have bounded densities
Statement
Assume the Axiom of Choice. If is a finite measure space and is bounded and complex-linear, then there is an essentially bounded complex measurable such that One may take . The pairing contains no conjugation. AC is used through the finite-measure real Radon–Nikodym representation supplier.
Facts & Assumptions
Under AC a bounded real functional on finite-measure , , has a real integrable density representing it on every bounded measurable representative (On a finite-measure space, a bounded functional is integration against its Radon-Nikodym density).
Complex integration is defined through real and imaginary parts (Integrable real and complex functions, and their integrals).
The assumed axiom is The Axiom of Choice.
Dominated convergence yields convergence under an integrable majorant (Dominated convergence).
for integrable complex (The modulus of an integral is bounded by the integral of the modulus).
Proof
Given: AC, the finite measure space and ; put .
Restrict and to real classes. They are real-linear with norm at most . F1 with , under F3, gives real representing them on bounded real measurable functions.
Fix either density and its real functional . For , set . Its indicator is in since the measure space is finite. Then , so . Apply the same reasoning to with the negative functional. Their countable union shows almost everywhere. Define ; it is measurable and almost everywhere. We may set it to zero on the explicitly determined null set where this bound fails.
For a bounded complex function with real bounded , complex linearity gives , using F2. For arbitrary , let , with zero value at . Then is bounded, pointwise and , so F4 gives . Boundedness of gives , while step 2.1 and F5 give . Passing to the limit proves the formula for all classes.
If , the same level-set argument gives almost everywhere; if , is the zero space and take . Indicator tests were used only on a finite-measure space, and truncations were explicitly defined. The full AC use is precisely F1, not a presumed complex duality theorem.
Depends on
Used by
Dependency tree · two levels
21 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
- Razvan Gelca, Functional Analysis; complete Chapter 7 reading recorded in batch coverage (standard reference, not scraped)