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.
Hilbert space
Definition
A real Hilbert space is a real inner-product space whose induced-length metric is complete: every Cauchy sequence in for the norm converges to a point of . A complex Hilbert space is a complex inner-product space with the same completeness property, so that a Hilbert space is exactly a real or complex inner-product space that is a Banach space for its induced norm (Banach space).
The completion convention is the Cauchy-sequence one. Banach space defines completeness by convergence of Cauchy sequences, and this page keeps that convention throughout. It is weaker than -completeness — the assertion that every decreasing sequence of nonempty closed subsets with diameters tending to zero has a nonempty intersection. The two agree in ZFC, but Blackadar, Farah and Karagila note that the closest-point theorem on a -complete inner-product space is provable in ZF, whereas the Cauchy-complete form used below consumes the Axiom of Countable Choice; nothing here silently imports the stronger notion.
Depends on
Used by
- Anchored iteratively regularized Gauss-Newton with finite discrepancy stopping Algorithm
- Geometric median of block means Algorithm
- Landweber iteration with discrepancy and budget statuses Algorithm
- Nonlinear Landweber iteration with discrepancy stopping Algorithm
- Projected online gradient descent Algorithm
- Unanchored Levenberg–Marquardt step with explicit early stopping Algorithm
- A separable infinite-dimensional Hilbert space is ℓ² Corollary
- Compact operator iff approximation numbers tend to zero Corollary
- Each vector has at most countably many nonzero isotypic components Corollary
- Every real-order Bessel-potential completion is Hilbert Corollary
- Finite rank operators are norm dense in compact Hilbert space operators Corollary
- Non-invertible elliptic shifts form a discrete set in the self-adjoint case Corollary
- Orthonormal eigenbasis for a compact self adjoint operator Corollary
- Quadratic spectral bounds control a self-adjoint parabolic semigroup Corollary
- Symmetric Lax--Milgram is energy minimisation Corollary
- The Dirichlet Laplacian generates an analytic heat semigroup Corollary
- The Lax--Milgram solution operator has norm at most 1/α Corollary
- Weak well-posedness for constant divergence-free convection Corollary
- A bounded form without coercivity need not be solvable Counterexample
- A coercive form need not be symmetric Counterexample
- A nonzero left-null datum passes the series test but is not in the range Counterexample
- A norm-closed nonconvex set need not be weakly closed Counterexample
- A smooth map can fail the tangential cone condition Counterexample
- An everywhere-defined closed operator on a Banach space is bounded Counterexample
- An inner-product space need not be complete Counterexample
- Coercive non-symmetric forms need not have an orthonormal eigenbasis Counterexample
- Infinitely many modes admit inequivalent irreducible regular Weyl representations Counterexample
- Nearest-point maps to convex sets need not be linear Counterexample
- The integers do not have property (T) Counterexample
- The L² unit sphere is not weakly sequentially closed in infinite dimensions Counterexample
- The Neumann Poisson problem is not coercive on all of H¹ Counterexample
- The unitary dual need not be Hausdorff Counterexample
- The universal Weyl C*-algebra has nonregular representations Counterexample
- A Borel prior concentrated on a forward-map domain Definition
- Absolute value and singular values of a compact operator Definition
- Adjoint of a densely defined operator Definition
- Almost invariant vectors for a unitary representation Definition
- Banach evolution triples and weak time derivatives Definition
- Bochner L2 space for a finite product-law input Definition
- Bounded, coercive and symmetric sesquilinear forms Definition
…and 298 more results.
Dependency tree · two levels
21 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, Definition 1.41, p.39 (standard reference, not scraped)
- Andrew Lin and Casey Rodriguez, MIT 18.102 Introduction to Functional Analysis, Lecture 16 (standard reference, not scraped)
- Bruce Blackadar, Ilijas Farah and Asaf Karagila, Hilbert spaces without the Countable Axiom of Choice, Definitions 1.0.1 and 2.0.1 (standard reference, not scraped)