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.
Distributions supported at one point
Statement
For and , if and only if for some finite and complex coefficients. The coefficients, with absent higher terms interpreted as zero, are unique. A nonzero such combination has support exactly ; the zero combination has empty support. This holds in ZF.
Facts & Assumptions
Dirac derivatives evaluate tests by (Dirac delta and its derivatives).
Compact support gives one finite-order estimate on a compact neighborhood for every test (Compactly supported distributions have global finite order). Two tests that agree on a neighborhood of the distributional support have equal pairings, and empty support is equivalent to the zero distribution (Support of a distribution).
Smooth compact cutoffs equal to one near a prescribed compact set exist in ZF (Test function cutoffs and euclidean localization).
On an open convex neighborhood, the Taylor remainder for a function is for (Multivariable Taylor formula with remainder). Apply separately to real and imaginary parts; for degree zero use continuity directly.
Proof
Given: and a distribution .
Suppose its support is contained in . Obtain an order and constant from F2. Take a fixed smooth equal to one near zero with support in a ball , using F3 in Euclidean space. For all sufficiently small , is supported inside and equals one near . Hence for every test.
Suppose for every . For fixed , Taylor's formula F4 on a ball about applied to gives ; when this is continuity with value zero. The little-o bounds are uniform over by their definition: their suprema are . The product rule expands a derivative of order , , of into finitely many terms [step 1.1, F2, F4, algebra] Each has supremum , hence tends to zero, even when . All derivatives vanish outside the shrinking support. Thus F2 and step 1.1 give , so .
Take a fixed cutoff equal to one near and compactly supported in . For put . Direct monomial differentiation gives for and zero for every other . Therefore has zero jet through degree . Step 2.1 makes its pairing zero, giving . By F1 this is the claimed representation with .
Conversely, every test supported in has all derivatives zero at , so F1 makes every displayed combination vanish there. Its support is therefore contained in . Evaluate a zero combination on the tests constructed with the largest order occurring to see each coefficient is zero. This proves uniqueness. Finally a nonzero distribution cannot have empty support by locality (as used in F2), so a nonzero combination has support exactly . The zero combination is allowed with . All jets and sums are finite and no choice is used.
Depends on
Used by
Nothing in the library uses this result yet.
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)