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.
Relative dual norming, point separation, and recovery of the norm
Statement
Assume HB and let be a real or complex normed space. For each there is with and , a positive real number also in the complex case. Hence separates distinct points, and The formula includes and the zero space. Moreover, if has norm-dense scalar-linear span and for all , then .
Facts & Assumptions
Under HB every bounded scalar-linear functional on a linear subspace extends preserving its norm (Relative norm-preserving Hahn–Banach extension over the real and complex fields).
A linear span consists exactly of finite linear combinations, including the empty combination zero ( is exactly the set of linear combinations of finite lists of elements of , and ).
Density means that the closure is the whole space; membership in the closure means that every positive-radius ball meets the set (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).
The norm on is (The dual space X^* of a normed space and its dual norm).
Proof
Given: HB, a real or complex normed space , and, for the last assertion, with norm-dense linear span.
Fix . The set contains zero and is closed under addition and scalar multiplication, so is a linear subspace. The coefficient of is unique: with would imply on multiplying by . Thus is well-defined and scalar-linear. Moreover and , so .
For the final assertion alone, suppose for all and the span of is norm dense. Every finite combination satisfies , including , so every element of the span vanishes at .
Apply norm-preserving extension to this and . Its hypotheses were checked in step 1.1, so it gives with and . This is an existence statement for the fixed .
For , apply step 2.1 to . The resulting functional satisfies , hence separates these points.
For any and , normalization gives ; for both sides vanish. Thus every unit-ball value is at most . For nonzero step 2.1 attains this upper bound; for the zero functional has norm zero and attains value zero. This proves the maximum formula even if .
Fix and . By density a ball of radius about meets the span, so there is in the span with . Thus . If and , taking is impossible; if , then already. Therefore all vanish at , and the maximum formula gives , hence .
Source notes
Brezis Corollaries 1.3–1.4, pp.3–4; Teschl Corollary 4.16 and Theorem 4.20 proof, pp.114–116.
Remarks
The maximum is over functionals for a fixed vector. It does not assert that each fixed functional attains its own norm on the unit ball, or that a simultaneous function has been selected.
Depends on
Relative norm-preserving Hahn–Banach extension over the real and complex fields
is exactly the set of linear combinations of finite lists of elements of , and
Interior, closure, boundary, limit point, isolated point and dense subset of a metric space
The dual space X^* of a normed space and its dual norm