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 distributions have global finite order
Statement
If has compact support , there are a compact neighborhood of , an integer and such that, for every , In particular one order exponent works on every fixed-support stage. The estimate is on a compact neighborhood, not necessarily on itself. The result holds in ZF.
Facts & Assumptions
Every distribution has a finite-order bound on each fixed compact support (Local finite order characterization of distributions).
Tests agreeing near the support of a distribution have equal pairings; empty support means zero distribution (Support of a distribution).
A compact subset of an open Euclidean set has a smooth compactly supported cutoff equal to one near it (Test function cutoffs and euclidean localization).
Proof
Given: with compact support .
If , F2 gives and take , , with the empty supremum zero. Otherwise take from F3 equal to one near and put . It is compactly inside and contains a neighborhood of . For every test , the test vanishes near , so by F2.
Apply F1 on the single compact to obtain with on . The finite product rule gives ; this follows by iterating the coordinate product rule, with coefficients combined by Pascal's identity. If , then . The derivatives of are bounded on , so is finite. Together with step 1.1 this gives the asserted estimate with .
If for another compact , all its derivatives vanish off , so the maximum over is at most . Thus the same exponent gives the global finite-order property (indeed the same works here). The proof selected only one cutoff and one finite-order witness pair and used no choice axiom.
Depends on
Used by
Dependency tree · two levels
8 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)