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.
Compact support continuous primitive representation
Statement
Assume AC. Let have compact support and global order at most . For every open with , there are finitely many continuous functions on , each compactly supported in , such that Zero functions may fill unused indices. Only the AC use in the local representation theorem is needed beyond the stated elementary operations.
Facts & Assumptions
Under AC, local representation by a continuous function can use the multi-index when the localized distribution has order bound (Local structure of distributions as derivatives of continuous functions).
Distributional Leibniz's rule holds for smooth multipliers (Leibniz rule for distributions).
A compact set inside an open set admits a smooth compact cutoff equal to one near it (Test function cutoffs and euclidean localization).
A compactly supported distribution pairs with smooth functions by cutoff, and vanishes on smooth functions zero near its support (Compactly supported distributions extend to smooth functions).
The assumed axiom is The Axiom of Choice.
Proof
Given: and AC.
Use F3 in to choose equal to one near , and put . By F1 and F5 there is continuous on with on , where each . For every test , F4 gives , and , hence globally on .
For any distribution , F2 implies the inverse product identity [step 1.1, F2, algebra] Indeed expand each derivative on the right by F2. The coefficient of is . The sum is the product of the binomial expansions of , so it is zero unless , when it is one. Thus precisely the left side remains.
Apply step 2.1 to and define . These functions are continuous and supported in . Multiplying a regular functional by the smooth factor yields its pointwise product by the defining integral, so step 1.1 and the identity give the required sum. There are only indices. If is empty, by support locality and all functions may be zero. For the bound is still . No further infinite selection occurs.
Depends on
Used by
Dependency tree · two levels
18 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
- Razvan Gelca, Functional Analysis (standard reference, not scraped)