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 as regular distributions
Definition
Assume Countable Choice for the published injection theorem. Let be open, with . For , its regular distribution is The integral is finite because is bounded and has compact support. The pairing is complex bilinear: there is no conjugation. It depends only on the almost-everywhere class of , and the induced map is complex-linear and injective. The pairing is the regular functional of Regular distribution from a locally integrable function, and the injection is Locally integrable functions embed in distributions under The Axiom of Countable Choice (). Countable Choice is used only for that published injectivity theorem; defining the pairing and its linearity require no choice. If , both spaces contain only zero and the map is the unique injection.
Well-definedness. If almost everywhere, then for each test function the integrands agree almost everywhere, so their integrals agree. The published continuity estimate makes every such regular functional a distribution; the published embedding theorem supplies the converse implication almost everywhere under Countable Choice.
Depends on
Used by
- A step has no locally integrable weak derivative Counterexample
- Cantor function has singular distributional derivative Counterexample
- Weak derivative of a locally integrable function Definition
- Absolute value has a Dirac second derivative Example
- Linearity, locality, and commutation of weak derivatives Lemma
- Uniqueness of a weak derivative as an almost-everywhere class Lemma
- Weak Leibniz rule with a smooth factor Lemma
- Weak derivatives are represented distributional derivatives Remark
Dependency tree · two levels
17 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
- Juha Kinnunen, Sobolev Spaces (2026), Chapter 1 §1.1 (standard reference, not scraped)
- Semyon Dyatlov, Lecture notes for 18.155 (2022), regular distributions (standard reference, not scraped)