LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge 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.

Finite-dimensional Auerbach bases

Statement

Every nonzero finite-dimensional real or complex normed space $V$ has a basis $(x_{1}, \dots, x_{n})$ with biorthogonal coordinate functionals $(x_{1}^{*}, \dots, x_{n}^{*})$ such that

$∥ x_{i} ∥ = ∥ x_{i}^{*} ∥ = 1 (1 \leq i \leq n) .$

Facts & Assumptions

[L1]

An ordered finite basis gives a topological coordinate isomorphism (A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space).

[L2]

Closed bounded subsets of finite-dimensional real coordinate space are compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

Proof

technique · extremal

Given: The objects and hypotheses in the Statement.

1.1

Fix a reference basis and use [L1] to identify $V^{n}$ with a finite real [given, L1, L2] coordinate space (of twice the dimension in the complex case). By [L2], the product of $n$ unit spheres is compact. The absolute determinant relative to the reference basis is continuous, so it attains a maximum there. The maximum is positive because the normalized reference basis is an admissible independent tuple. Let $(x_{1}, \dots, x_{n})$ maximize it.

L1L2choose

2.1

The positive determinant makes $(x_{i})$ a basis, and each $∥ x_{i} ∥ = 1$ by construction. For any unit $y$ and fixed $i$ , multilinearity gives

givenstep 1.1

$∣ \det (x_{1}, \dots, y, \dots, x_{n}) ∣ = ∣ x_{i}^{*} (y) ∣ ∣ \det (x_{1}, \dots, x_{i}, \dots, x_{n}) ∣ .$

Maximality therefore gives $∣ x_{i}^{*} (y) ∣ \leq 1$ , so $∥ x_{i}^{*} ∥ \leq 1$ . Since $x_{i}^{*} (x_{i}) = 1$ and $∥ x_{i} ∥ = 1$ , the reverse inequality holds. [step 1.1, determinant multilinearity]

3.1

The argument selects one maximizer from one nonempty compact set and does [given, step 2.1] not select bases for a family of spaces. Thus it uses no choice principle.

step 1.12.1∎

Depends on

Used by

The Dvoretzky--Rogers finite-block estimate Lemma

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

Thomas Schlumprecht, Course Notes in Functional Analysis, Math 655 (standard reference, not scraped)