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.
An inner-product space need not be complete
Statement refuted
Every inner-product space is complete for its induced norm.
Facts & Assumptions
The -series converges, and a convergent sequence of reals is Cauchy (For rational , converges iff , Every convergent sequence is Cauchy, Limits and Cauchy sequences of reals).
On counting measure the integral of is the series of the , and almost-everywhere equality is equality everywhere, so the norm of a finitely supported sequence is ( is the space of counting measure, Counting measure on an arbitrary set).
The pairing is linear in the first argument, conjugate-linear in the second and positive definite, and Cauchy–Schwarz gives (Real and complex inner-product spaces and their induced length, Cauchy–Schwarz: , with equality exactly for dependent pairs).
A metric space is complete when every Cauchy sequence converges in it, and a Hilbert space is complete for its induced norm (Complete metric space: every Cauchy sequence converges in the space, Hilbert space).
Counterexample
Given: The space of finitely supported real or complex sequences with the pairing , a finite sum for .
The pairing is an inner product on : linearity in the first argument and conjugate symmetry are finite-sum algebra, and forces every coordinate to vanish; the induced length is the norm of the finitely supported sequence.
Let be the sequence with for and for ; each lies in , and for one has , a difference of partial sums of the convergent -series, which tends to as by [A1]; hence is Cauchy in the norm.
Suppose were a limit of in the induced norm; then for each fixed , Cauchy–Schwarz applied to and the -th coordinate vector gives , so for every , and has infinitely many nonzero coordinates, contrary to finite support.
Hence the Cauchy sequence in the inner-product space has no limit there, so is not complete for its induced norm, and the statement that every inner-product space is complete is false.
Depends on
- Real and complex inner-product spaces and their induced length
- Cauchy–Schwarz: $|\langle x,y\rangle|\le\|x\|\,\|y\|$, with equality exactly for dependent pairs
- For rational $p > 0$, $\sum 1/k^p$ converges iff $p > 1$
- $\ell^p$ is the $L^p$ space of counting measure
- Counting measure on an arbitrary set
- Every convergent sequence is Cauchy
- Complete metric space: every Cauchy sequence converges in the space
- Hilbert space
- Limits and Cauchy sequences of reals
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
55 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 Salamon, Functional Analysis, §1.3.3 and §2.3.6 (standard reference, not scraped)
- Andrew Lin and Casey Rodriguez, MIT 18.102 Introduction to Functional Analysis, Lecture 16 (standard reference, not scraped)