Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02
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 n≥1, k∈N0, 1≤p<∞ and K∈{R,C}. Then the compactly supported smooth functions Cc∞(Rn;K) are dense in Wk,p(Rn;K): for every u∈Wk,p(Rn;K) and every δ>0 there is φ∈Cc∞(Rn;K) with ∥φ−u∥Wk,p(Rn)<δ. No such norm-density assertion is made for p=∞.

Facts & Assumptions

Given: Countable Choice; k∈N0; 1≤p<∞; K∈{R,C}; a class u∈Wk,p(Rn;K); and a tolerance δ>0.

[F1]

Cutoff bumps: for 0<r<R there is χ∈Cc∞(Rn;[0,1]) with χ=1 on B‾r(0) and supp⁡χ⊆BR(0) (A smooth bump between concentric Euclidean balls); fix such a χ with r=1 and outer radius 2. For χR(x):=χ(x/R) one has χR=1 on B‾R(0), supp⁡χR⊆B2R(0), and, by the chain rule, ∥DβχR∥L∞(Rn)≤CβR−∣β∣ for 1≤∣β∣≤k with constants depending only on k and the fixed bump.

[F2]

Smooth-factor Leibniz rule: χRu∈Wk,p(Rn;K) for every ∣α∣≤k, with Dα(χRu)=∑β≤α(αβ)(DβχR)Dα−βu almost everywhere (Weak Leibniz rule with a smooth factor).

[F3]

Dominated convergence: if gR→g almost everywhere and ∣gR∣≤G for a single integrable G, then ∫gR→∫g (Dominated convergence).

[F4]

Interior mollification: for f∈Wk,p(Rn;K) and a nonnegative unit-mass bump ρ supported in B‾1(0), the mollifications fε=ρε∗f are smooth on Rn with Dαfε=ρε∗(Dαf) for every ∣α∣≤k; if f is compactly supported then so is fε (Interior mollification commutes with weak derivatives, The mollifier family generated by a unit-mass smooth bump).

[F5]

Approximate identity convergence for finite p: with (ρε) a mollifier family, ρε∗f→f in Lp(Rn;K) for every f∈Lp(Rn;K) and 1≤p<∞, for real and complex scalars alike (A unit-mass smooth bump generates an L1 approximate identity, Every L1 approximate identity converges to the identity in Lp for 1≤p<∞, Complex translation, convolution, approximate identities, and mollification).

[F6]

The norm of Wk,p(Rn;K) is the ℓp sum of the Lp norms of Dαu, ∣α∣≤k (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

technique · direct
1.1F1F2given

Fix the cutoff family χR of [F1]. For each R>0 the function χRu satisfies the hypotheses of [F2] with η=χR, so χRu∈Wk,p(Rn;K) and Dα(χRu)=χRDαu+∑0≠β≤α(αβ)(DβχR)Dα−βu; in particular χRu is compactly supported, with support in B2R(0).

2.1F1F3F6step 1.1

Large-R convergence. For each ∣α∣≤k, Dα(χRu)−Dαu=(χR−1)Dαu+∑0≠β≤α(αβ)(DβχR)Dα−βu. The first term tends to 0 in Lp by [F3], since (χR−1)Dαu→0 pointwise as R→∞ and its p-th power is bounded by 2p∣Dαu∣p∈L1; each remaining term is bounded in Lp by CβR−∣β∣∥Dα−βu∥Lp, which tends to 0. Summing over the finitely many ∣α∣≤k and using [F6], there is R with ∥χRu−u∥Wk,p(Rn)<δ2.

3.1step 2.1

Fix such an R and write f:=χRu, a compactly supported class in Wk,p(Rn;K); then ∥f−u∥Wk,p(Rn)<δ/2 and supp⁡f⊆B2R(0).

4.1F1F4step 3.1

Mollification. Fix a nonnegative unit-mass ρ∈Cc∞(Rn) supported in B‾1(0), obtained by normalizing a bump from [F1] with inner radius 1/2 and outer radius 1. For every 0<ε<1 the function fε=ρε∗f lies in Cc∞(Rn;K) (smoothness and support in B2R+ε(0) by [F4]), and Dαfε=ρε∗(Dαf) for every ∣α∣≤k.

5.1F5F6step 3.1step 4.1∎

Convergence of the mollified approximants: for each ∣α∣≤k, the class Dαf lies in Lp(Rn;K) and [F5] gives ∥Dαfε−Dαf∥Lp→0 as ε→0+; summing over ∣α∣≤k with [F6], choose ε>0 with ∥fε−f∥Wk,p(Rn)<δ/2. Then φ:=fε∈Cc∞(Rn;K) satisfies ∥φ−u∥Wk,p≤∥φ−f∥Wk,p+∥f−u∥Wk,p<δ by steps 3.1 and 4.1. Since u and δ were arbitrary, Cc∞(Rn;K) is dense; the hypothesis p<∞ enters exactly here, and no assertion is made for p=∞.

Depends on

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