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.
Locally integrable functions embed in distributions
Statement
Assume the Axiom of Countable Choice. The map , , is a complex-linear injection from modulo almost-everywhere equality into . It is continuous from the local topology, generated by for compact , to the strong distribution topology. In particular local convergence implies strong distribution convergence. The continuity estimate itself is choice-free; Countable Choice is used in the cited approximate-identity theorem proving injectivity.
Facts & Assumptions
The regular functional is well-defined modulo almost-everywhere equality and satisfies on (Regular distribution from a locally integrable function).
Compactwise finite-order bounds characterize distributions (Local finite order characterization of distributions).
A unit-mass smooth bump has rescalings (The mollifier family generated by a unit-mass smooth bump); these form an approximate identity under Countable Choice (A unit-mass smooth bump generates an approximate identity).
Under Countable Choice, convolution by such an approximate identity converges to each in (Every approximate identity converges to the identity in for , with ).
Smooth nonnegative compact cutoffs equal to one near a compact set exist (Test function cutoffs and euclidean localization).
Strong seminorms are uniform pairings over bounded test sets, which have common compact support and bounded derivative suprema (Weak and strong topologies on distributions).
Dominated convergence gives convergence for almost-everywhere convergent functions under one integrable majorant (Dominated convergence).
The assumed choice principle is The Axiom of Countable Choice ().
Proof
Given: Countable Choice and a locally integrable function on .
F1 and F2 show is a distribution, with compactwise order at most zero; linearity of the integral gives linearity in the equivalence class of . For a bounded test set , take its common compact and finite . Then . Thus each strong seminorm of the image is bounded by a constant times a defining local seminorm, proving continuity, including for nets. If , the left side is zero.
Suppose , and fix a closed ball compactly inside . Take from F5 equal to one near and compactly supported in , and extend by zero to ; it is in by local integrability. Also use F5 to obtain a nonnegative smooth compact bump equal to one on a ball, and divide it by its positive finite integral to obtain of mass one. Fix containing its support. For sufficiently small , every has inside the neighborhood where : the compact has positive distance from that neighborhood's closed complement. Consequently [step 1.1, given, F3, F5] The integrals are absolutely finite because and the kernel is bounded; the reflected kernel is a test compactly supported in .
By F3, F4 and F8, . Since on and step 2.1 makes the convolution zero there, . Hence almost everywhere on . The closed rational balls compactly inside are countable and their interiors cover ; applying this conclusion to each and taking the countable union of the null sets gives almost everywhere on . No family of cutoffs was selected simultaneously. Apply the same argument to for injectivity of the map on equivalence classes.
As a useful convergence consequence, if almost everywhere and for every compact there is an integrable majorant of all on , F7 gives . Step 1.1 then gives strong convergence . On the empty domain there is only the zero class and zero distribution, so injection and continuity still hold.
Depends on
Regular distribution from a locally integrable function
Local finite order characterization of distributions
The mollifier family generated by a unit-mass smooth bump
Every approximate identity converges to the identity in for
Dominated convergence
Test function cutoffs and euclidean localization
Weak and strong topologies on distributions
The Axiom of Countable Choice ()
A unit-mass smooth bump generates an approximate identity