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.
Compactly supported smooth functions are dense in W^{k,p}(R^n)
Statement
Assume Countable Choice. Let , , and . Then the compactly supported smooth functions are dense in : for every and every there is with No such norm-density assertion is made for .
Facts & Assumptions
Given: Countable Choice; ; ; ; a class ; and a tolerance .
Cutoff bumps: for there is with on and (A smooth bump between concentric Euclidean balls); fix such a with and outer radius . For one has on , , and, by the chain rule, for with constants depending only on and the fixed bump.
Smooth-factor Leibniz rule: for every , with almost everywhere (Weak Leibniz rule with a smooth factor).
Dominated convergence: if almost everywhere and for a single integrable , then (Dominated convergence).
Interior mollification: for and a nonnegative unit-mass bump supported in , the mollifications are smooth on with for every ; if is compactly supported then so is (Interior mollification commutes with weak derivatives, The mollifier family generated by a unit-mass smooth bump).
Approximate identity convergence for finite : with a mollifier family, in for every and , for real and complex scalars alike (A unit-mass smooth bump generates an approximate identity, Every approximate identity converges to the identity in for , Complex translation, convolution, approximate identities, and mollification).
The norm of is the sum of the norms of , (Integer-order Sobolev spaces and their norms).
Choice use. Countable Choice is used through the mollification and approximate-identity interfaces of [F4]–[F5]; the cutoffs of [F1] and the dominated-convergence argument of step 2.1 are explicit.
Proof
Fix the cutoff family of [F1]. For each the function satisfies the hypotheses of [F2] with , so and ; in particular is compactly supported, with support in .
Large- convergence. For each , The first term tends to in by [F3], since pointwise as and its -th power is bounded by ; each remaining term is bounded in by , which tends to . Summing over the finitely many and using [F6], there is with
Fix such an and write , a compactly supported class in ; then and .
Mollification. Fix a nonnegative unit-mass supported in , obtained by normalizing a bump from [F1] with inner radius and outer radius . For every the function lies in (smoothness and support in by [F4]), and for every .
Convergence of the mollified approximants: for each , the class lies in and [F5] gives as ; summing over with [F6], choose with . Then satisfies by steps 3.1 and 4.1. Since and were arbitrary, is dense; the hypothesis enters exactly here, and no assertion is made for .
Depends on
- Meyers–Serrin density on an arbitrary open set
- Weak Leibniz rule with a smooth factor
- Interior mollification commutes with weak derivatives
- The mollifier family generated by a unit-mass smooth bump
- A unit-mass smooth bump generates an $L^1$ approximate identity
- Every $L^1$ approximate identity converges to the identity in $L^p$ for $1 \le p < \infty$
- Complex translation, convolution, approximate identities, and mollification
- Dominated convergence
- A smooth bump between concentric Euclidean balls
- Integer-order Sobolev spaces and their norms
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Dependency tree · two levels
66 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
- Juha Kinnunen, Sobolev Spaces (2026), Theorem 1.21 and Remark 1.22(1) (standard reference, not scraped)
- Richard S. Laugesen, Linear Analysis and Partial Differential Equations (2020), Theorem 3.9 (standard reference, not scraped)