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 Lp duality from real Lp duality
Statement
Assume the Axiom of Countable Choice . Let be any measure space, let , and let be conjugate to . Every bounded complex-linear functional has a unique such that
where the pairing is bilinear, with no conjugation. Moreover .
Facts & Assumptions
Given: , an arbitrary measure space, conjugate exponents , and a bounded complex-linear .
Under Countable Choice, every bounded real-linear functional on real over an arbitrary measure space is uniquely integration against a real density, with equality of norms (For , the same representation theorem holds on arbitrary measure spaces).
Complex is the a.e. quotient of measurable finite-valued complex functions with finite -norm; real and imaginary parts, conjugation, products, and positive powers have the stated measurability conventions, and bilinear tests use without conjugation (Complex Lp classes and Euclidean test-function conventions).
Complex Hölder makes the bilinear pairing bounded, and complex has the quotient norm with (Complex Holder, Minkowski, and the quotient norm).
Countable Choice selects from every countable family of nonempty sets (The Axiom of Countable Choice ()).
Proof
Regard real as the real-valued subspace of complex . The maps and are bounded real-linear functionals there, with . Applying [F1] twice gives real such that and for every real . Put ; component inequalities in [F3] make its -norm finite.
For real-valued , componentwise complex integration gives . If is an arbitrary complex class, [F3] puts its real and imaginary parts in real , and complex linearity gives . All identities depend only on a.e. classes by the quotient and integration conventions in [F2]–[F3].
Hölder [F3] gives , hence . If a.e., step 2.1 gives and equality follows. Otherwise define on and where . Then and pointwise. Since , [F2]–[F3] give , , and . Testing on proves , including the closed unit-norm endpoint.
If gives the same pairing functional, put . Then for every . If were nonzero, the phase test of step 3.1 with in place of would produce with , a contradiction. Thus in , so the density is unique.
Steps 2.1–4.1 prove existence, equality of norms, and uniqueness. Countable Choice is used only inside the real arbitrary-measure representation [F1], whose construction makes countably many local choices; applying that theorem to and requires only two instances and no stronger choice principle. The empty and zero-measure spaces have only zero classes and are covered by the branch of step 3.1; the forbidden endpoints never enter because .
Remarks
The absence of a conjugate in the displayed pairing is deliberate. It is why the phase test contains : multiplication then gives the nonnegative real function .
Depends on
Used by
Dependency tree · two levels
37 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. (standard reference, not scraped)
- Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)