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.
Tensor product distributions and iterated pairings
Statement
For and the tensor candidate is a distribution on , uniquely determined by . Its two iterated pairing orders agree, and . Three-factor pairings associate. Moreover and . All claims hold in ZF.
Facts & Assumptions
The tensor candidate is well-defined and linear, and has the stated values on product tests (Tensor product of distributions).
Compactwise finite-order estimates characterize distributions (Local finite order characterization of distributions).
Parameter differentiation passes through a distribution pairing with locally common compact supports (Distribution pairing with smooth parameter families).
Finite product-test sums are dense in the product LF test space with a common compact support (Finite sums of product tests are dense on product open sets).
Support is the complement of the largest vanishing open set (Support of a distribution), and vanishing on an open cover implies vanishing on its union (Distributions form a sheaf).
Distribution derivatives are signed test transposes (Distributional derivative).
Proof
Given: the distributions on the open factor domains.
Fix compact and let be its compact projections. F2 gives bounds for on and for on . For , the inner paired function has support in by F1, and F3 gives its derivatives by pairing derivatives of . Applying the two bounds yields . F2 proves it is a distribution. The same argument applies with the pairing order reversed.
The two orders have the same values on all products by F1. Their difference is a continuous functional zero on all finite product sums, so F4 makes it zero on every test. The same reasoning shows uniqueness of any distribution with the product values.
If , choose an open neighborhood of on which . On tests supported in , the outer test in F1 is supported compactly in , so the tensor vanishes. If , the reversed pairing of step 2.1 gives the corresponding vanishing near . F5 proves support containment in the product. Conversely, if lies in that product, every open neighborhood contains with . F5 implies there exist tests , with nonzero pairings; otherwise one factor would vanish on that neighborhood. F1 makes their product pairing nonzero. Thus the tensor does not vanish on any neighborhood of , proving equality of supports. Only two local witnesses were used.
Applying the distribution construction to two blocks at a time gives distributions and on a triple product, each taking value on pure triple tests. To prove equality, fix : their difference on is a continuous functional in , since multiplying by this fixed test preserves compact support and bounds derivatives by fixed constants. F4 in makes it zero for every . F4 again, now for , makes the original difference zero on every triple test. This proves associativity and agreement of the nested orders.
For the derivative, F6 applied to the outer distribution and F3 applied to the inner test give , the asserted derivative. For the derivative apply F6 directly to the inner pairing. If a factor is zero, all formulas give zero and the support product is empty; empty domains behave the same way. Order-zero derivatives are identities. All estimates and density passages were choice-free.
Depends on
Used by
Dependency tree · two levels
25 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)