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.
Riesz representation for Hilbert spaces
Statement
Assume the Axiom of Countable Choice. Let be a real or complex Hilbert space and let be a bounded linear functional on (The dual space X^* of a normed space and its dual norm). Then there is a unique with
and , where is the dual norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum). Under the first-variable-linear convention the representing vector depends conjugate-linearly and isometrically on : if is represented by and are scalars, then is represented by .
Facts & Assumptions
If is a bounded linear functional then and , and exactly when (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces).
Cauchy–Schwarz gives , and the pairing is linear in the first argument and conjugate-linear in the second with (Cauchy–Schwarz: , with equality exactly for dependent pairs, Real and complex inner-product spaces and their induced length).
The kernel of a bounded linear functional is either all of or a proper linear subspace, and the orthogonal complement of a subspace is closed under the decomposition for closed (Linear subspace of a vector space, Orthogonal decomposition by a closed subspace).
For a subset , (Orthogonality and the orthogonal complement).
Countable Choice is the hypothesis under which the orthogonal decomposition, and hence this representation, is obtained (The Axiom of Countable Choice ()).
Proof
Given: Countable Choice, a real or complex Hilbert space and a bounded linear functional on .
If , then represents because for every , and ; the same has no other representing vector, since a vector representing satisfies and hence .
If , its kernel is a proper linear subspace of : it is linear because , it is proper because takes a nonzero value, and it is closed because and give .
Choose with and put , so ; decompose with and , then shows and .
For arbitrary , the vector satisfies , hence and ; moreover , so with .
Norm and uniqueness: Cauchy–Schwarz gives , so , while gives ; hence , and this contains the case . If also for all , then for all , and the choice gives , so .
Conjugate linearity: if for , then for all and scalars one has by conjugate-linearity in the second argument; uniqueness of the representing vector therefore gives the representing vector , so the map is conjugate-linear, and by step 4.1 it is isometric.
Steps 1.1, 3.1 and 4.1 produce the unique representing vector together with the norm identity for every bounded , and step 5.1 records its conjugate-linear isometric dependence; Countable Choice is used exactly through the orthogonal decomposition of step 2.1.
Depends on
- Orthogonal decomposition by a closed subspace
- Cauchy–Schwarz: $|\langle x,y\rangle|\le\|x\|\,\|y\|$, with equality exactly for dependent pairs
- The dual space X^* of a normed space and its dual norm
- A bounded linear operator between normed spaces
- The operator norm as the least bound and as the unit-sphere or unit-ball supremum
- Linear subspace of a vector space
- Orthogonality and the orthogonal complement
- Real and complex inner-product spaces and their induced length
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- Hilbert spaces are reflexive Corollary
- Adjoint of a densely defined operator Definition
- Relative compactness with respect to an operator Definition
- The Hilbert-space adjoint of a bounded operator Definition
- Continuous functional calculus produces a regular PVM Lemma
- Lax–Milgram is owned by the PDE track Remark
- Weyl criterion for the essential spectrum Theorem
Dependency tree · two levels
35 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
- Theo Bühler and Dietmar Salamon, Functional Analysis, Theorems 1.43 and 5.35, pp.39 and 236 (standard reference, not scraped)
- Andrew Lin and Casey Rodriguez, MIT 18.102 Introduction to Functional Analysis, Theorem 184 (standard reference, not scraped)
- Bruce Blackadar, Ilijas Farah and Asaf Karagila, Hilbert spaces without the Countable Axiom of Choice, Theorem 2.0.6 (standard reference, not scraped)