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.
Convolution with a test function is smooth
Statement
Let and . On the open safe domain , the convolution is smooth and The last expression is restricted to if its own safe domain is larger. For the domain is all of . This holds in ZF.
Facts & Assumptions
The convolution is on its open safe domain (Convolution of a distribution with a test function).
A smooth parameter family with locally common compact test support pairs smoothly with a distribution, and parameter derivatives pass through the pairing (Distribution pairing with smooth parameter families).
Distribution derivatives act by signed test differentiation (Distributional derivative).
Proof
Given: as in the statement.
Put . For compact , all -supports of , , lie in . This is compact as the continuous image of the compact product , and it lies in by the definition of . The function is jointly smooth, so F2 gives smoothness of and .
Differentiating the reflected test in gives . F3 therefore gives , since the two signs multiply to one. Together with step 1.1 this proves both equalities.
The support of is contained in , so its safe domain contains , justifying the stated restriction. If , the safe domain is all of and each expression is zero. If is empty the smoothness and equalities are vacuous on that open set; gives the defining convolution identity. No choice is used.
Depends on
Used by
Dependency tree · two levels
13 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
- Semyon Dyatlov, Lecture notes for 18.155 (2022) (standard reference, not scraped)