Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Smooth compact supports are dense in Schwartz space

Statement

For f∈S(Rn) and the preceding cutoff, χ(x/R)f(x)∈Cc∞ and tends to f in every Schwartz seminorm as R→∞. Thus Cc∞ is dense in the topology of Schwartz topology and convergence. This is choice-free.

Facts & Assumptions

[F1]

The cutoff equals one on the unit ball, vanishes outside radius two, and its dilated derivatives have factor R−∣γ∣ (Explicit compactly supported smooth cutoffs).

[F2]

The one-variable higher product rule holds (The general Leibniz rule for the n-th derivative of a product).

Proof

technique · direct
1.1F2F3givenalgebra

Apply [F2] successively in each coordinate and use [F3] to regroup derivatives; for complex functions apply the real rule to the four real products. This gives ∂β(uv)=∑γ≤β(βγ)(∂γu)(∂β−γv), where (βγ)=∏j<n(βjγj). Also, on ∣x∣≥R, ∣x∣≤∑j<n∣xj∣ gives ∣xα∂δf(x)∣≤R−1∑j<npα+ej,δ(f). Indeed multiply the left side by ∣x∣ and bound each ∣xjxα∂δf∣ by its seminorm.

2.1step 1.1F1given∎

For u=χR−1, [F1] makes the undifferentiated product-rule term vanish on ∣x∣≤R and have coefficient at most one elsewhere. For γ≠0, ∂γχR is supported on R≤∣x∣≤2R, with supremum R−∣γ∣Cγ, Cγ=∥∂γχ∥∞<∞. Boundedness follows from continuity on its compact support. Hence for R≥1 the formula in step 1.1 gives pαβ((χR−1)f)≤R−1∑j<npα+ej,β(f)+∑0≠γ≤β(βγ)CγR−1−∣γ∣∑j<npα+ej,β−γ(f). This tends to zero. The product is smooth with compact support inside the dilated support of χ; each weighted derivative is bounded on that compact set, so χRf∈Cc∞⊆S. Taking the explicit integers R=1,2,… proves density.

Depends on

Dependency tree · 2 levels

Sources