LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09

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.

Complex completeness, density, and inner product: the consumer interface

Statement

Assume countable choice. On every measure space, complex $L^{p}$ is complete for $1 \leq p \leq \infty$ , and every norm-convergent sequence has a subsequence of measurable representatives converging a.e. to its limit. For finite $p$ , finite simple functions with finite-measure support are dense, and on $R^{n}$ with Lebesgue measure, $n \geq 1$ , complex $C_{c}^{\infty}$ is dense. Complex $L^{2}$ has the first-variable-linear inner product $\int f \overline{g}$ , its norm is $∥ \cdot ∥_{2}$ , and Cauchy–Schwarz has the following equality criterion: if $g \neq 0$ , equality iff $f = c g$ a.e.; if $g = 0$ , equality for all $f$ . 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.

[F1]

Complex Lp completeness and a.e. subsequences hold under countable choice (Complex Lp completeness and almost-everywhere subsequences).

[F2]

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).

[F3]

The $L^{2}$ form has the stated norm and equality criterion, also for finite tuples (The complex $L^{2}$ pairing is well-defined and satisfies Cauchy–Schwarz).

Proof

technique · Apply the separate completeness, density and pairing theorems with their exact hypotheses

1.1

The measure space and exponent satisfy F1, and the assumed countable choice is exactly its additional hypothesis. It therefore supplies completeness for every $1 \leq p \leq \infty$ and a.e.-convergent subsequences with the specified limit class.

F1given

1.2

For $p < \infty$ , 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.

F2given

2.1

For $p = 2$ , F3 proves that the representative formula descends to an inner product and that its squared norm equals $\int ∣ f ∣^{2}$ . Thus its induced norm is the same $L^{2}$ 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.

F3step 1.1∎

Depends on

Used by

Complex translation, convolution, approximate identities, and mollification Lemma

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)