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.
A compact diagonal map with dense nonclosed range
Example
Assume the Axiom of Countable Choice. On the real Hilbert space , define the diagonal map for , where and is the coordinate vector at . In positive indexing, its singular system is and for . Then is compact and its range is dense but not closed. The datum lies in and in , but not in ; its Picard sum diverges, so the equation has no exact solution.
Example references
Facts & Assumptions
Given: Countable Choice and with the map .
For , the canonical pairing is , the norm satisfies , and is the sequence equal to at and elsewhere. Whenever , every admits a finite set with (Square-summable families on an arbitrary index set and the space ).
is complete and hence a real Hilbert space (The real square-summable sequence space is complete, Hilbert space).
A bounded linear map with finite-dimensional range is compact (Bounded finite rank operators are compact).
Under Countable Choice, a norm limit of compact maps into a Banach space is compact (Norm limit of compact operators is compact).
For a compact operator with singular values and complete positive singular vectors , exact range membership is equivalent to orthogonality to and finiteness of the Picard sum (Picard range and pseudoinverse-domain criterion).
The series converges (The p-series for a real exponent p converges exactly when p is greater than one).
For every real there is with (For every in a complete ordered field there is a natural with ).
The compact linear inverse model has Hilbert parameter/data spaces and a compact forward map, and exact data have the form (Compact linear inverse model between Hilbert spaces).
The Hilbert adjoint is characterized by (The Hilbert-space adjoint of a bounded operator).
Countable Choice is required by [F4] and by the compact singular-system theorem used in [F5], and is the hypothesis of [F9] (The Axiom of Countable Choice ()).
Proof
The map is linear and satisfies , so it is bounded. For , let when and otherwise. The estimate makes bounded, and its range is spanned by the finite ordered family : every output has no coordinates beyond , and for each , while these coordinate vectors are linearly independent. Thus they form an ordered basis of the range, and is compact by [F3]. For every , , with equality in the operator norm at . Hence . By [F2] the codomain is Banach, so [F4] gives compactness of . It is a compact inverse model by [F8].
Every finitely supported belongs to : set , which is finitely supported and satisfies . For any and , [F1] gives a finite set with ; choose containing . Then the truncation supported on indices obeys . Thus finitely supported vectors are dense, and since all lie in , is dense in .
For , [F6] gives . Its finite truncations are in by step 1.2 and converge to because the tails of its square-sum tend to zero; hence . If , then every coordinate equation gives , contradicting . Indeed, if the finite sums had an upper bound , [F7] with would give , and the partial sum at would exceed . Therefore and the dense range is not closed.
The coordinate vectors are orthonormal because [F1] gives when and otherwise. They are complete: for any and , [F1] gives a finite set with ; choose containing , so the truncation's squared error is at most this tail. Direct calculation gives and by step 1.2. For , the canonical inner product gives ; hence [F9] identifies . Since all diagonal coefficients are positive, . Therefore and , and the family is complete on both and . Reindexing by gives the positive singular system , for . The datum has , so every Picard summand equals . For any real bound , [F7] applied with gives an index , so the corresponding finite subsums are unbounded and the Picard sum diverges, as [F5] predicts for a datum outside the range.
Depends on
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The Hilbert-space adjoint of a bounded operator
- Hilbert space
- Compact linear inverse model between Hilbert spaces
- The natural numbers $\mathbb{N}$ (von Neumann)
- Square-summable families on an arbitrary index set and the space $\ell^2(I)$
- Bounded finite rank operators are compact
- The real square-summable sequence space is complete
- Picard range and pseudoinverse-domain criterion
- Norm limit of compact operators is compact
- The p-series for a real exponent p converges exactly when p is greater than one
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
84 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
- Christian Clason, Regularization of Inverse Problems: Lecture Notes, arXiv:2001.00617v2, Theorems 3.9–3.10, §§3.1–3.2 (standard reference, not scraped)
- Vesa Kaarnioja, Inverse Problems: Fourth Lecture, FU Berlin, 8 May 2023, PDF pp. 10–12 (standard reference, not scraped)