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

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.

Simultaneous L1 and L2 smooth approximation

Statement

Assume countable choice and let $n \geq 1$ . For $f \in L^{1} (R^{n}; C) \cap L^{2} (R^{n}; C)$ there is one sequence $f_{j} \in C_{c}^{\infty}$ converging to $f$ in both norms.

Facts & Assumptions

Given: An integer $n \geq 1$ and The Axiom of Countable Choice ( ${A C}_{ω}$ ). The real approximate-identity, smoothness, support and rescaling suppliers are Every $L^{1}$ approximate identity converges to the identity in $L^{p}$ for $1 \leq p < \infty$ , Convolution with a mollifier is smooth, and derivatives pass under the integral sign, The support of a convolution lies in the closure of the support sumset, and A unit-mass smooth bump generates an $L^{1}$ approximate identity.

[F1]

Dominated convergence holds (Dominated convergence).

[F2]

Under countable choice in dimension $n \geq 1$ , the complex interface gives convergence of mollifications in each finite-exponent norm, and smooth compact support for a compactly supported input (Complex translation, convolution, approximate identities, and mollification).

[F3]

There is an explicit nonnegative smooth cutoff equal to one on the unit ball and supported in the radius-two ball (Explicit compactly supported smooth cutoffs).

Proof

technique · direct

1.1

Fix a finite measurable representative of $f$ and set $g_{j} = f 1_{{∣ x ∣ \leq j, ∣ f (x) ∣ \leq j}}$ , $j \geq 1$ . Then $g_{j}$ is bounded and compactly supported, and $∣ g_{j} - f ∣^{p} \leq ∣ f ∣^{p}$ tends pointwise to zero for $p = 1, 2$ . [F1] therefore gives $∥ g_{j} - f ∥_{p} \to 0$ in both norms. Let $χ$ be [F3]'s cutoff and put $ρ = χ / \int χ$ . Its integral is finite since it is bounded and supported in a finite-volume ball, and positive since it equals one on a ball containing a positive-volume box. Thus $ρ$ is a specified real smooth compactly supported kernel of mass one.

F1F3given

2.1

For fixed $j$ , [F2] gives $ρ_{1 / k} * g_{j} \to g_{j}$ as $k \to \infty$ in both norms. Let $k_{j}$ be the least positive integer for which both errors are below $1 / j$ , and define $f_{j} = ρ_{1 / k_{j}} * g_{j}$ . The qualifying set is nonempty since both convergences hold, and the least-integer rule needs no further choice. [F2] makes $f_{j}$ smooth with compact support (contained in the radius $j + 2 / k_{j}$ ball). Finally $∥ f_{j} - f ∥_{p} \leq 1 / j + ∥ g_{j} - f ∥_{p} \to 0$ for both $p = 1, 2$ . The same sequence works, with countable choice inherited only from the Euclidean mollification interface.

step 1.1F2given∎

Depends on

Used by

Agreement of the integral and L2 transforms Theorem

Dependency tree · two levels

49 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 (2017) (standard reference, not scraped)