Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09
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 X be a real or complex normed space. For each x≠0 there is f∈X∗ with ∥f∥=1 and f(x)=∥x∥, a positive real number also in the complex case. Hence X∗ separates distinct points, and ∥x∥=max⁡f∈X∗, ∥f∥≤1∣f(x)∣(x∈X). The formula includes x=0 and the zero space. Moreover, if H⊆X∗ has norm-dense scalar-linear span and h(x)=0 for all h∈H, then x=0.

Facts & Assumptions

[F1]

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).

[F2]

A linear span consists exactly of finite linear combinations, including the empty combination zero (span⁡(S) is exactly the set of linear combinations of finite lists of elements of S, and span⁡(∅)={0V}).

[F3]

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).

[F4]

The norm on X∗ is sup⁡∥y∥≤1∣f(y)∣ (The dual space X^* of a normed space and its dual norm).

Proof

Given: HB, a real or complex normed space X, and, for the last assertion, H⊆X∗ with norm-dense linear span.

1.1givenF4algebra

Fix x≠0. The set M=Kx contains zero and is closed under addition and scalar multiplication, so is a linear subspace. The coefficient of x is unique: (a−b)x=0 with a≠b would imply x=0 on multiplying by (a−b)−1. Thus g(ax)=a∥x∥ is well-defined and scalar-linear. Moreover ∣g(ax)∣=∣a∣∥x∥=∥ax∥ and g(x/∥x∥)=1, so ∥g∥=1.

1.2givenF2algebra

For the final assertion alone, suppose h(x)=0 for all h∈H and the span of H is norm dense. Every finite combination g=∑j<najhj satisfies g(x)=∑j<najhj(x)=0, including n=0, so every element of the span vanishes at x.

2.1step 1.1F1

Apply norm-preserving extension to this M and g. Its hypotheses were checked in step 1.1, so it gives f∈X∗ with ∥f∥=1 and f(x)=g(x)=∥x∥. This is an existence statement for the fixed x.

3.1step 2.1algebra

For v≠w, apply step 2.1 to x=v−w≠0. The resulting functional satisfies f(v)−f(w)=f(v−w)=∥v−w∥>0, hence separates these points.

3.2step 2.1F4algebra

For any h∈X∗ and x≠0, normalization gives ∣h(x)∣=∥x∥∣h(x/∥x∥)∣≤∥h∥∥x∥; for x=0 both sides vanish. Thus every unit-ball value is at most ∥x∥. For nonzero x step 2.1 attains this upper bound; for x=0 the zero functional has norm zero and attains value zero. This proves the maximum formula even if X={0}.

4.1step 3.2step 1.2F3algebra∎

Fix f∈X∗ and ε>0. By density a ball of radius ε about f meets the span, so there is g in the span with ∥f−g∥<ε. Thus ∣f(x)∣=∣(f−g)(x)∣≤∥f−g∥∥x∥≤ε∥x∥. If ∥x∥>0 and ∣f(x)∣>0, taking ε=∣f(x)∣/(2∥x∥) is impossible; if ∥x∥=0, then x=0 already. Therefore all f vanish at x, and the maximum formula gives ∥x∥=0, hence x=0.

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 x↦fx has been selected.

Depends on

Used by

Dependency tree · two levels

24 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