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.
Complex completeness, density, and inner product: the consumer interface
Statement
Assume countable choice. On every measure space, complex is complete for , and every norm-convergent sequence has a subsequence of measurable representatives converging a.e. to its limit. For finite , finite simple functions with finite-measure support are dense, and on with Lebesgue measure, , complex is dense. Complex has the first-variable-linear inner product , its norm is , and Cauchy–Schwarz has the following equality criterion: if , equality iff a.e.; if , equality for all . The finite-tuple version uses a common scalar across components.
Facts & Assumptions
Given: Countable choice, an arbitrary measure space and exponents in the stated ranges; Euclidean Lebesgue measure for smooth density.
Complex Lp completeness and a.e. subsequences hold under countable choice (Complex Lp completeness and almost-everywhere subsequences).
Finite-simple density holds on arbitrary spaces and smooth density under countable choice on Euclidean spaces, both for finite p (Complex finite-simple and smooth compact-support density for finite p).
The form has the stated norm and equality criterion, also for finite tuples (The complex pairing is well-defined and satisfies Cauchy–Schwarz).
Proof
The measure space and exponent satisfy F1, and the assumed countable choice is exactly its additional hypothesis. It therefore supplies completeness for every and a.e.-convergent subsequences with the specified limit class.
For , F2 applies to the same measure space and gives finite-simple approximants with finite-measure nonzero sets. In the Euclidean clause its Lebesgue and countable-choice hypotheses also hold, so it supplies smooth compactly supported approximants.
For , F3 proves that the representative formula descends to an inner product and that its squared norm equals . Thus its induced norm is the same norm used in step 1.1. F3 also supplies precisely the nonzero-second-argument scalar-multiple criterion and the zero-second-argument exception, and its finite-sum proof supplies the common-scalar tuple version. This collects the asserted interfaces without any additional analytic hypothesis.
Depends on
Used by
- Conjugate duality of Hˢ and H⁻ˢ Corollary
- Every real-order Bessel-potential completion is Hilbert Corollary
- The n-dimensional Heisenberg uncertainty inequality Corollary
- Hermitian metric and L² pairing on a compact Riemann surface Definition
- Lp Fourier multiplier and its norm Definition
- Spatial and frequency centres and variances of an L² function with finite second moments Definition
- The maximal Dolbeault operator and its Hilbert adjoint on a compact Riemann surface Definition
- Weighted Fourier candidate norm on Schwartz space Definition
- A Dirac mass has precisely sufficiently negative Sobolev order Example
- Adjoints of shifts, multiplication and integral operators Example
- Circular Radon inversion at the zero truth Example
- Diagonal operator on ell p is compact iff diagonal tends to zero Example
- Normalized Hermite Fourier eigenfunctions Example
- Spectrum of a multiplication operator Example
- Spectrum of the unilateral shift Example
- The Gaussian attains equality in the Heisenberg inequality Example
- The standard inner products make K n, ell two and quotient L two Hilbert spaces Example
- Bessel potentials shift Sobolev order Lemma
- Centring by translation and modulation preserves the variance product Lemma
- Completeness of normalized probabilists’ Hermite polynomials in Gaussian L² Lemma
- Complex translation, convolution, approximate identities, and mollification Lemma
- Continuity of bivariate Gaussian feature expectations, including singular limits Lemma
- L² with the integral pairing is a Hilbert space Lemma
- Real L2 multipliers and unitary transport Lemma
- Schwartz space is dense in L2 Lemma
- The coordinate inequality ‖xⱼf‖₂‖Dⱼf‖₂≥1/2‖f‖₂² Lemma
- The weighted discrete-series space is a Hilbert space with K-type basis Lemma
- Agreement of the integral and L2 transforms Theorem
- Carleson maximal operator is strong ltwo Theorem
- Gårding estimates for the Dolbeault Laplacian on a compact Riemann surface Theorem
- Heisenberg uncertainty and Gaussian equality Theorem
- L2 Fourier inversion Theorem
- Plancherel theorem Theorem
- The Bessel completion embeds canonically in tempered distributions Theorem
Dependency tree · two levels
18 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
- Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)