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 bounded complex linear functional on a subspace of a complex normed space extends with the same norm
Statement
Assume the Axiom of Choice. Let be a complex normed space, let be a linear subspace, and let be a bounded complex linear functional. Then there exists a bounded complex linear functional such that and .
Facts & Assumptions
Given: The Axiom of Choice, A complex normed space , a linear subspace , and a bounded complex linear functional .
AC is used through the real extension supplier [L1] in step 2.1.
A bounded real linear functional on a real normed subspace extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).
A complex linear functional is recovered from its real part by , and conversely every such formula defines a complex linear functional (A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)).
The complex norm axioms are those of Complex norm and complex normed space. The same norm is a real norm on realification (Realification preserves a complex norm and its metric); a complex-linear subspace carries its restricted complex norm (A complex normed linear subspace) and realifies to a real normed subspace with the same norm and restricted metric (A complex normed subspace and its finite basis realify).
Proof
Let . By [L2], is real linear on the underlying real subspace . Also so is bounded with .
Apply [L1] to the underlying real normed spaces. This yields a bounded real linear functional extending and satisfying . Define By [L2], is complex linear and .
For , the equality and [L2] give So extends .
Fix . Choose so that is a nonnegative real number. Since and is complex linear, Therefore where the last inequality uses step 1.1 and . Hence .
Since , every with satisfies . Taking the supremum over the unit ball of gives . Combined with step 3.2, this yields .
Depends on
- The Axiom of Choice
- A bounded real linear functional on a subspace of a real normed space extends with the same norm
- A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)
- Complex norm and complex normed space
- Realification preserves a complex norm and its metric
- A complex normed linear subspace
- A complex normed subspace and its finite basis realify
Used by
- C star state GNS construction, purity and Polish pure-state spaces Lemma
- Irreducible representations separate arbitrary C star algebras Lemma
- The norm of a positive element is the supremum of its state values Lemma
- Tracial standard form, normal functional vectors, and expectation Lemma
- A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed Theorem
- Every nonzero vector has a norming functional Theorem
- Reflexive approximation property implies metric approximation property Theorem
- Reflexive spaces have the Radon--Nikodym property Theorem
Dependency tree · two levels
26 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
- Daniel Daners, Introduction to Functional Analysis, Theorem 26.4 (standard reference, not scraped)
- Gerald Teschl, Topics in Real and Functional Analysis, Theorem 4.14 (standard reference, not scraped)