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 form a sheaf
Statement
For an open inclusion , restriction of a distribution is defined by testing on the smooth zero extension of a test in . These restrictions are distributions and compose as restrictions do for functions. For any open cover of , distributions agreeing on every overlap glue to a unique . This holds in ZF for an arbitrary index set .
Facts & Assumptions
Distributions are complex-linear continuous test functionals (Distribution).
Continuity is equivalent to a finite-order estimate on each fixed compact support (Local finite order characterization of distributions).
Multiplication by a smooth function preserves tests; its derivative estimates follow from the finite product rule used to justify Multiplication of a distribution by a smooth function.
Every open cover has an at most countable locally finite smooth partition with compact supports, each support contained in some cover member, without selecting labels (Test function cutoffs and euclidean localization).
Proof
Given: the cover and compatible family in the statement.
For and , its support is compactly inside , so extension by zero is smooth on . On each compact its derivative seminorms are unchanged. The bound of F2 for on therefore gives that bound for its restriction; this proves restriction is a distribution. Testing successive zero extensions proves composition and identity of restrictions.
Take the partition of F4. For each and each test , the test has compact support inside any member containing . Its evaluation by that member's distribution is independent of the member: two such members overlap on its support, so compatibility applies. Denote this uniquely specified number by ; this definition selects no labels. Set . Only finitely many partition supports meet : local finiteness provides neighborhoods meeting finitely many supports, and a finite subcover of the compact support suffices. Thus the sum exists. Applying the same finite set to the union of two test supports proves complex linearity.
Fix compact . Only finitely many partition supports meet . For these finitely many indices take containing cover members and their finite-order bounds on the compact supports of the corresponding . Finite choices are provable by finite induction in ZF. Let be the maximum of their orders, or zero if none occur. The finite product rule gives [step 2.1, F2, F3] where derivatives of vanish off . Summing the finitely many bounds yields with finite . Hence is a distribution by F2.
If , every nonzero summand is evaluated on a test with compact support in and a containing cover member. Compatibility makes it . The finite sum is since . Thus the restrictions are the prescribed ones. If a distribution restricts to zero on each , the same finite decomposition gives for every test. Applying this to the difference of two glued distributions proves uniqueness, and therefore independence of the partition. For the empty cover of the empty domain the sum defines the zero distribution and uniqueness still holds.
Depends on
Used by
- Support of a distribution Definition
- Convolution of distributions is well defined under the support hypothesis Lemma
- A distribution with zero derivatives on a connected open set is constant Theorem
- Extension by zero for distributions with ambient closed support Theorem
- Global locally finite structure of distributions Theorem
- Tensor product distributions and iterated pairings Theorem
Dependency tree · two levels
9 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)