ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Norm-attaining functionals on a Hilbert space

Statement

Assume the Axiom of Countable Choice. Let $H$ be a real or complex Hilbert space, meaning an inner product space complete for its induced norm. Every bounded linear functional $f \in H^{*}$ attains its norm on the closed unit ball. More precisely, if $f \neq 0$ , then there is a unique $y \in H ∖ {0}$ such that

$f (x) = ⟨ x, y ⟩ (x \in H),$

and $f$ attains its norm at $y / ∥ y ∥$ . The zero functional is represented by $y = 0$ and attains its norm at every point of the closed unit ball.

Facts & Assumptions

Given: The Axiom of Countable Choice ${A C}_{ω}$ , a real or complex Hilbert space $H$ , and a bounded linear functional $f \in H^{*}$ .

[F1]

The inner product is linear in its first variable, conjugate-linear in its second, conjugate symmetric, and positive definite (Real and complex inner product spaces, with the inner product linear in the first argument). It induces the norm $∥ x ∥ = \sqrt{⟨ x, x ⟩}$ (The norm $∥ v ∥ = \sqrt{⟨ v, v ⟩}$ induced by a real or complex inner product), which is definite, homogeneous, and satisfies the triangle inequality (The inner-product norm is definite, homogeneous, and satisfies the triangle inequality).

[F2]

Completeness for the norm metric makes $H$ a Banach space (Banach space). The dual $H^{*}$ consists of bounded scalar-linear functionals and has norm $∥ f ∥ = \sup_{∥ x ∥ \leq 1} ∣ f (x) ∣$ (The dual space X^* of a normed space and its dual norm). Consequently $∣ f (x) ∣ \leq ∥ f ∥ ∥ x ∥$ for every $x \in H$ .

[F3]

Every nonempty real set bounded below has an infimum, and if $d$ is that infimum then for every $η > 0$ the set contains a point smaller than $d + η$ (Every nonempty set bounded below has an infimum, Epsilon characterisation of the infimum).

[F4]

For every positive real $η$ some reciprocal $1 / n$ is smaller than $η$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[F5]

A closed linear subspace of a Banach space is Banach (A closed subspace of a Banach space is Banach).

[F6]

Countable Choice selects one element from every member of an $N$ -indexed family of nonempty sets (The Axiom of Countable Choice ( ${A C}_{ω}$ )). It is used below only to select the countable sequence of approximate minimizers.

[F7]

Cauchy–Schwarz gives $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ in either scalar field (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

Proof

technique · Construct the Riesz vector as the shortest point of an affine hyperplane, proving existence of that point from a countably chosen minimizing sequence and the parallelogram identity

1.1F1F2

If $f = 0$ , take $y = 0$ . Then $f (x) = ⟨ x, 0 ⟩$ and $∥ f ∥ = 0 = ∣ f (x) ∣$ for every $x$ in the closed unit ball, including $x = 0$ when $H = {0}$ . Hence assume from now on that $f \neq 0$ ; in particular $H \neq {0}$ and $∥ f ∥ > 0$ .

1.2F1F2F5

Choose $w \in H$ with $f (w) \neq 0$ and put $v = w / f (w)$ , so $f (v) = 1$ . Let $M = \ker f$ . It is a linear subspace, and the following estimate proves that it is closed and hence Banach.

Indeed, if $x \notin M$ , then

$r = \frac{∣ f (x) ∣}{2 ∥ f ∥} > 0,$

and $∥ h - x ∥ < r$ implies

$∣ f (h) ∣ \geq ∣ f (x) ∣ - ∣ f (h - x) ∣ > ∣ f (x) ∣ - ∥ f ∥ r = \frac{∣ f (x) ∣}{2} > 0.$

Thus the open ball $B (x, r)$ misses $M$ , so the complement of $M$ is open. By [F5], $M$ is therefore a Banach space with the restricted norm. [F1, F2, F5]

2.1step 1.2F2F3

The set $D = {∥ v - u ∥ : u \in M}$ is nonempty (take $u = 0$ ) and bounded below by $0$ , so [F3] gives $d = \inf D$ ; the functional estimate below also proves that this infimum is positive.

For every $u \in M$ ,

$1 = ∣ f (v - u) ∣ \leq ∥ f ∥ ∥ v - u ∥,$

and hence $d \geq 1 / ∥ f ∥ > 0$ . [step 1.2, F2, F3]

3.1step 2.1F3F6

For each natural $n$ , define the following set of approximate minimizers and use Countable Choice to select from all of them.

$A_{n} = {u \in M : ∥ v - u ∥ < d + \frac{1}{n + 1}} .$

Each $A_{n}$ is nonempty by [F3]. Apply ${A C}_{ω}$ once to this family and choose $m_{n} \in A_{n}$ for every $n$ . Thus, with $r_{n} = ∥ v - m_{n} ∥$ ,

$d \leq r_{n} < d + \frac{1}{n + 1} .$

This is the sole use of choice in the proof. [F3, F6]

4.1step 2.1step 3.1F1

Put $a_{n} = v - m_{n}$ . Expanding squared norms and using that the kernel contains midpoints gives the estimate below.

$∥ a_{n} - a_{k} ∥^{2} + ∥ a_{n} + a_{k} ∥^{2} = 2 ∥ a_{n} ∥^{2} + 2 ∥ a_{k} ∥^{2} .$

Since $(m_{n} + m_{k}) / 2 \in M$ , the definition of $d$ gives $∥ (a_{n} + a_{k}) / 2 ∥ \geq d$ . Therefore

$\begin{matrix} ∥ m_{n} - m_{k} ∥^{2} \leq 2 r_{n}^{2} + 2 r_{k}^{2} - 4 d^{2} . & (1) \end{matrix}$

This is the estimate used below. [step 2.1, step 3.1, F1]

5.1step 3.1step 4.1F4

The sequence $(m_{n})$ is Cauchy by the following explicit use of the reciprocal bound in the estimate from step 4.1.

Given $ε > 0$ , set

$η = \min {1, \frac{ε^{2}}{8 d + 4}} > 0.$

By [F4], choose $N$ so that $1 / (N + 1) < η$ . For $n, k \geq N$ , step 3.1 and the eventual monotonicity of reciprocals give $r_{n}, r_{k} < d + η$ . Using $η \leq 1$ in (1),

$∥ m_{n} - m_{k} ∥^{2} < 4 (d + η)^{2} - 4 d^{2} = 8 d η + 4 η^{2} \leq (8 d + 4) η \leq ε^{2} .$

Both sides before squaring are nonnegative, so $∥ m_{n} - m_{k} ∥ < ε$ . [step 3.1, step 4.1, F4]

6.1step 1.2step 2.1step 3.1step 5.1F1F4F5

Since $M$ is Banach, $m_{n} \to m$ for some $m \in M$ ; the minimizing bounds and triangle inequality show that this limit realizes the infimum.

The triangle inequality gives

$d \leq ∥ v - m ∥ \leq ∥ v - m_{n} ∥ + ∥ m_{n} - m ∥ .$

Given $ε > 0$ , step 3.1, [F4], and convergence let us make the two terms on the right smaller than $d + ε / 2$ and $ε / 2$ , respectively. Thus $∥ v - m ∥ < d + ε$ for every $ε > 0$ , while $d$ is a lower bound, so $∥ v - m ∥ = d$ . [step 1.2, step 2.1, step 3.1, step 5.1, F1, F4, F5]

7.1step 2.1step 6.1F1

Set $z = v - m$ . Then $f (z) = 1$ , and $z \neq 0$ because $∥ z ∥ = d > 0$ ; real variations, and then the $i u$ variation over the complex field, prove that $z$ is orthogonal to the kernel.

For $u \in M$ and $t \in R$ , minimality of $m$ and $m + t u \in M$ give

$\begin{matrix} ∥ z - t u ∥^{2} - ∥ z ∥^{2} = t^{2} ∥ u ∥^{2} - 2 t Re ⟨ z, u ⟩ \geq 0. & (2) \end{matrix}$

If $Re ⟨ z, u ⟩ \neq 0$ , then $u \neq 0$ and taking $t = Re ⟨ z, u ⟩ / ∥ u ∥^{2}$ makes the right side of (2) negative. Hence $Re ⟨ z, u ⟩ = 0$ . Over $C$ , apply the same conclusion to $i u \in M$ ; the linear-first convention gives $⟨ z, i u ⟩ = - i ⟨ z, u ⟩$ , whose real part is $Im ⟨ z, u ⟩$ . Thus in either scalar field $⟨ z, u ⟩ = 0$ for every $u \in M$ . [step 2.1, step 6.1, F1]

8.1step 7.1F1

For arbitrary $x \in H$ , subtracting $f (x) z$ puts the remainder in the kernel and yields the unique representing vector.

Indeed, the vector $u = x - f (x) z$ lies in $M$ . Step 7.1 and conjugate symmetry give $⟨ u, z ⟩ = 0$ , so

$⟨ x, z ⟩ = f (x) ∥ z ∥^{2} .$

Consequently, with $y = z / ∥ z ∥^{2}$ ,

$f (x) = ⟨ x, y ⟩ (x \in H) .$

If another vector $y^{'}$ represented $f$ , then $⟨ x, y - y^{'} ⟩ = 0$ for all $x$ ; choosing $x = y - y^{'}$ and using positive definiteness gives $y = y^{'}$ . [step 7.1, F1]

9.1step 1.1step 8.1F1F2F7

Cauchy–Schwarz supplies the upper bound, and evaluation at the normalized representing vector supplies equality and norm attainment.

By [F7], $∣ f (x) ∣ \leq ∥ x ∥ ∥ y ∥$ , so $∥ f ∥ \leq ∥ y ∥$ . Conversely the unit vector $x_{0} = y / ∥ y ∥$ satisfies

$f (x_{0}) = ⟨ \frac{y}{∥ y ∥}, y ⟩ = ∥ y ∥,$

where the last number is positive real. Thus $∥ f ∥ = ∥ y ∥ = ∣ f (x_{0}) ∣$ , and $f$ attains its norm at $x_{0}$ . Together with the zero case in step 1.1, this proves every clause, including both scalar fields and the zero Hilbert space. [step 1.1, step 8.1, F1, F2, F7] ∎

Remarks

The construction is a local proof of the Riesz representation needed for this example; it does not cite the later Hilbert-space geometry page. The argument is choice-free except for the one $N$ -indexed selection in step 3.1, which is why the statement explicitly assumes ${A C}_{ω}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 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 A. Salamon, Functional Analysis (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)