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.
Pullback of a distribution by a diffeomorphism
Definition
Let be an integer, let be a smooth diffeomorphism between open subsets of , and let in the convention of Distribution. Put . The chain rule applied to makes invertible, so . It is smooth: the determinant is smooth and nonzero, and its sign is locally constant. Define The transformed test has support in , a compact subset of . Multiplication by the fixed smooth reciprocal Jacobian and diffeomorphic composition are continuous linear test operations by Test function operations are continuous, so their transpose defines a distribution. This definition is choice-free. For the identity map the Jacobian is one and the pullback is the identity; the zero distribution pulls back to zero. Empty diffeomorphic domains give zero test and distribution spaces. The absolute value of the determinant handles orientation reversal; arbitrary smooth maps are not covered by this definition.
For compatibility with functions, use the regular-functional convention of Regular distribution from a locally integrable function and assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). If and is compact, put . This is an function. The exact formula of A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions gives The formula also makes the transformed integrand measurable; since is positive and its reciprocal is bounded on , this proves . If almost everywhere, apply the same formula to , whose integral is zero, and use A nonnegative measurable function has integral exactly when it vanishes almost everywhere to obtain almost everywhere on each compact . Thus composition respects local almost-everywhere classes. For a fixed test , the function is integrable, since its smooth factor is bounded with compact support. Applying the same change-of-variables formula gives Thus , with both regular functionals distributions by Locally integrable functions embed in distributions. Countable Choice is used through the published Lebesgue change-of-variables and embedding results, not through the definition of .
Depends on
- Distribution
- Regular distribution from a locally integrable function
- Locally integrable functions embed in distributions
- Test function operations are continuous
- A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions
- A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
44 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)