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.
Distribution pairing with smooth parameter families
Statement
Let be integers, let and be open, let , and let . Suppose that for each compact there is compact with for every . Then is smooth and .
Assume Countable Choice for the following integral clause. For every compact measurable , the function is a test in , its derivatives pass under the integral, and . Integrals here are Lebesgue integrals. The smoothness and differentiation claims hold in ZF; Countable Choice supplies Lebesgue measure for the integral clause. Neither clause uses tensor products or distributional mollification.
Facts & Assumptions
On each , has a finite-order estimate (Local finite order characterization of distributions).
Smooth test operations preserve compact support and commute as ordinary partial derivatives (Test function operations are continuous).
Each is complete in its derivative-seminorm metric (Fixed support test function spaces are complete).
A compact parameter set has a smooth compact cutoff equal to one near it (Test function cutoffs and euclidean localization).
The mean-value inequality bounds the increment of a differentiable vector-valued curve by its length times a bound on its derivative; use (The mean value inequality: if is continuous and differentiable on with , then ).
Absolute integrals bound moduli of integrals (The modulus of an integral is bounded by the integral of the modulus), and integration is complex-linear on (The Lebesgue integral is linear on ).
Countable Choice supplies complete Lebesgue measure and finite box volumes (The Axiom of Countable Choice (), Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume).
Proof
Given: integers , , and the compact-support hypothesis.
Around a fixed take a closed ball with a slightly larger closed ball still inside . The hypothesis on the larger ball supplies a single compact for all its slices. Every parameter derivative of has support in for parameters in the smaller ball: for the function is identically zero for all parameters in a neighborhood, so all parameter derivatives vanish there. On the smaller ball times , every mixed derivative is uniformly continuous by compactness. Thus for each , and F1 gives continuity of .
Fix a coordinate . For each , apply F5 on the segment from to (reverse its orientation if ) to the curve . The derivative increment is bounded uniformly in by a modulus of continuity tending to zero with . Dividing the resulting inequality by proves [step 1.1, F1, F2, F5] The F1 estimate passes this limit through . Apply step 1.1 to the parameter derivative slices for continuity of the resulting derivative, and repeat for every multi-index. This proves smoothness and the derivative formula.
For this clause assume Countable Choice and use F7 for Lebesgue measure. Fix compact . By F4 choose a smooth cutoff near with compact parameter support in . Extend by zero to all parameter space. It is smooth, and the support hypothesis on gives a common compact for all its slices and their derivatives. Choose a closed box whose interior contains that parameter support. At level divide each side into equal pieces, disjointify the cells by assigning shared faces in coordinate order, and let be each cell's lower corner. Put [step 2.1, given, F2, F4, F6, F7] These are tests supported in . For every , uniform continuity of the finitely many derivatives through order on supplies a modulus . For each derivative and fixed , F6 bounds the error between the grid sum and its scalar integral over by . The finite sum is exactly the integral of the corresponding step function, and its weights are finite because lies in a bounded box.
Comparing two grid sums via their scalar integrals gives . Thus F3 gives a limit . The degree-zero scalar error in step 3.1 identifies , and its higher-degree errors identify every derivative of with the corresponding integral. By F1, . By finite linearity , which converges to by the same uniform-continuity integral estimate, since step 2.1 makes that scalar function smooth. This proves interchange. Empty or measure-zero gives zero sums and integrals; empty gives zero slices. All tags and grids are specified, not chosen from an infinite family.
Depends on
- Local finite order characterization of distributions
- Test function operations are continuous
- Fixed support test function spaces are complete
- Test function cutoffs and euclidean localization
- The mean value inequality: if $f : [a,b] \to \mathbb{R}^m$ is continuous and differentiable on $(a,b)$ with $\lVert f'\rVert_2 \le M$, then $\lVert f(b)-f(a)\rVert_2 \le M(b-a)$
- The modulus of an integral is bounded by the integral of the modulus
- The Lebesgue integral is linear on $L^1(\mu)$
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Assuming countable choice, $\mathcal{L}(\mathbb{R}^n)$ is a sigma-algebra containing every elementary set and $\lambda_n$ is a complete measure extending elementary volume
Used by
- Smooth functions are weakly dense in distributions Corollary
- Tensor product of distributions Definition
- Compact distribution convolution preserves schwartz and tempered spaces Lemma
- Convolution with a test function is smooth Theorem
- Fourier transform of a compactly supported distribution is a smooth polynomially bounded multiplier Theorem
- Mollifier approximation in distributions Theorem
- Tensor product distributions and iterated pairings Theorem
- Translation invariant test function operators are convolutions Theorem
Dependency tree · two levels
61 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)