Alphabeta MathHow 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.
A separable Banach space has a countable norming family
Statement
Assume HB and countable choice. Let be a real separable Banach space. There is a sequence with such that If , the conclusion is interpreted using the zero functional and the supremum is .
Facts & Assumptions
Separability supplies a countable dense subset of (Separability: the existence of an at most countable dense subset).
For each nonzero , Hahn–Banach supplies with and (The real dominated-extension principle as an additional hypothesis over ZF, Relative dual norming, point separation, and recovery of the norm).
Countable choice selects one such functional for each element of a countable dense subset (The Axiom of Countable Choice ()).
Proof
Given: HB, countable choice, and a real separable Banach space .
If , take the constant zero sequence. Otherwise let be a countable dense subset of . The normalized set is countable and dense in the unit sphere: for and , eventually and . Enumerate it as . By [F2] and [A1], choose with and for each .
For every and every , , so the supremum is at most . If , choose unit vectors . Then , so . The zero vector gives equality directly.
Depends on
- Separability: the existence of an at most countable dense subset
- The dual space X^* of a normed space and its dual norm
- The real dominated-extension principle as an additional hypothesis over ZF
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Relative dual norming, point separation, and recovery of the norm
Used by
- Uncorrelated jointly Gaussian Banach random elements are independent Lemma
- Borell concentration for the norm of a separable Banach Gaussian Theorem
- Cameron–Martin translation formula for a separable Banach Gaussian Theorem
- Fernique integrability for a separable Banach Gaussian law Theorem
- Gaussian concentration-function sieve bounds Theorem
- Gaussian-process posterior contraction in density and regression models Theorem
- The support of a Banach Gaussian is the closure of its RKHS Theorem
Dependency tree · two levels
20 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
- A. Lunardi, M. Miranda, and D. Pallara, Infinite Dimensional Analysis (standard reference, not scraped)