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.
Not every distribution is a locally integrable function
Statement refuted
Every distribution on , , is represented by a locally integrable function. Under Countable Choice, is a counterexample.
Facts & Assumptions
Under Countable Choice the regular-distribution map is injective on almost-everywhere classes on every open domain (Locally integrable functions embed in distributions, The Axiom of Countable Choice ()).
Dirac is a distribution and (Dirac delta and its derivatives).
A test equal to one near zero exists (Test function cutoffs and euclidean localization).
A point is Lebesgue null, as a subset of a coordinate hyperplane (A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in ).
Proof
Given: Countable Choice and the witness .
Suppose with . On the open domain , all tests evaluate to zero at the origin, so F2 gives . F1 applied on this entire open domain, without selecting pointwise neighborhoods, gives almost everywhere on . By F4 the omitted singleton is null, so almost everywhere on .
Consequently , but F3 supplies with , and F2 gives . This contradiction proves that the witness is not regular and refutes the proposed universal statement. The zero function does represent the zero distribution; the failure is the nonzero point mass, not a failure of the regular-distribution construction. Dimension zero is excluded, since its singleton has mass one in the library convention.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
30 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)