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.
Convolution with a mollifier is smooth, and derivatives pass under the integral sign
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()).
Let be locally integrable, let have mass , and let be the associated mollifier. Then for every , the convolution
is smooth, and for every multi-index ,
Facts & Assumptions
Given: Countable Choice, a locally integrable function , a unit-mass smooth bump, and .
The mollifier family is defined in The mollifier family generated by a unit-mass smooth bump.
Differentiation under the integral sign is available (Differentiation under the integral sign).
Multi-index notation and Euclidean smoothness are fixed in maps and multi-index derivative notation in Euclidean space.
Products and sums of finite measurable real functions are measurable; applying this to real and imaginary parts gives the complex version (Arithmetic and lattice operations preserve measurability whenever they are defined).
Dominated convergence passes pointwise limits through integrals under an integrable absolute majorant (Dominated convergence).
Under Countable Choice, Lebesgue measure is a complete measure, so the integral theorems apply on its measure space (Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume).
Proof
Fix and . Choose with and put . Every derivative of vanishes off its support. Thus, for , all translated kernel derivatives vanish when . Each derivative is bounded by a finite constant , since it is continuous with compact support.
For each multi-index define . At fixed , the integrand is Lebesgue measurable by [L4], because is measurable and the translated kernel derivative is continuous. On its absolute value is bounded by , which is integrable by local integrability. Consequently every is well-defined. If in , continuity of the kernel gives pointwise convergence of the integrands; [L5] with this same majorant gives . Thus every is continuous locally, hence globally since was arbitrary.
Fix and a coordinate . For , the integrand is integrable, differentiable in , and has measurable derivative. The derivative is bounded by on this interval. Therefore [L2] yields . This identity holds for every .
Since , repeated use of step 3.1 gives every ordered iterated derivative of as the integral of against the corresponding derivative of the smooth kernel. All these integrals are continuous by step 2.1. Hence by [L3], and in particular for every multi-index .
Depends on
- The mollifier family generated by a unit-mass smooth bump
- Arithmetic and lattice operations preserve measurability whenever they are defined
- Differentiation under the integral sign
- Dominated convergence
- $C^k$ maps and multi-index derivative notation in Euclidean space
- 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
- Hilbert transform does not map L-infinity to L-infinity Counterexample
- Hilbert transform is not strong type (1,1) Counterexample
- Mollifying a zero extension leaks across the boundary Counterexample
- Weighted L2 spaces and maximal dbar operators Definition
- Hilbert transform of an interval indicator Example
- Mollifying 1_[0,1] at two scales Example
- The weak Dirichlet Poisson problem on an interval Example
- A compact C¹ leaf has finitely generated fundamental group Lemma
- A first saddle lobe admits a collar-fixed center-saddle cancellation Lemma
- Complex translation, convolution, approximate identities, and mollification Lemma
- Finite C2 surface carriers have smooth normal forms and relative cap approximations Lemma
- Heat-ball representation formula Lemma
- Immersion extension on a disk: absolute and relative parametric forms Lemma
- Interior mollification commutes with weak derivatives Lemma
- Mean-zero Poincare estimate on bounded connected extension domains below the dimension Lemma
- Mollification rates for compactly supported Slobodeckij functions Lemma
- Simultaneous L1 and L2 smooth approximation Lemma
- Smooth compactly supported functions of an open set are dense in L² Lemma
- Smoothing continuous families of formal immersions Lemma
- Smoothing continuous families of genuine immersions Lemma
- The inverse of a quasiconformal map is quasiconformal with the same dilatation Lemma
- The maximal distributional dbar operator is closed and densely defined Lemma
- C_c^∞(ℝⁿ) is dense in Lᵖ(ℝⁿ) for 1 ≤ p < ∞ Theorem
- Continuous ball-mean-value functions are harmonic Theorem
- Existence of bounded Kruzhkov entropy solutions Theorem
- Global Schauder regularity for the weak Dirichlet Laplacian Theorem
- Multidimensional Ito formula for Brownian-driven processes Theorem
- Oleinik's one-sided estimate characterizes bounded entropy solutions Theorem
- One-dimensional Ito formula Theorem
- Plancherel support for SL2(R) Theorem
- Smale–Hirsch for open source manifolds Theorem
- Space-time harmonic functions yield Brownian local martingales up to exit lifetime Theorem
- The distributional Riesz functional of a subharmonic function is a positive Radon measure Theorem
- The Fr'echet--Kolmogorov compactness criterion in Lᵖ(ℝⁿ) Theorem
- The Hamilton--Jacobi correspondence in one dimension Theorem
- The measurable Riemann mapping theorem on the sphere Theorem
- The Mihlin–Hörmander Fourier multiplier theorem Theorem
- The principle of descent and the logarithmic domination principle Theorem
- Zero weak gradient gives componentwise constants Theorem
Dependency tree · two levels
45 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
- Richard L. Wheeden and Antoni Zygmund, Measure and Integral: An Introduction to Real Analysis (standard reference, not scraped)