Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-08 (Codex)
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 (ACω)).

Let f:Rn→C be locally integrable, let φ∈Cc∞(Rn) have mass 1, and let φε be the associated mollifier. Then for every ε>0, the convolution

(f∗φε)(x):=∫Rnf(y)φε(x−y) dy

is smooth, and for every multi-index α,

∂α(f∗φε)=f∗(∂αφε).

Facts & Assumptions

Given: Countable Choice, a locally integrable function f, a unit-mass smooth bump, and ε>0.

[L1]
[L2]

Differentiation under the integral sign is available (Differentiation under the integral sign).

[L3]

Multi-index notation and Euclidean smoothness are fixed in Ck maps and multi-index derivative notation in Euclidean space.

[L4]

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).

[L5]

Dominated convergence passes pointwise limits through integrals under an integrable absolute majorant (Dominated convergence).

[L6]

Under Countable Choice, Lebesgue measure is a complete measure, so the integral theorems apply on its measure space (Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn is a complete measure extending elementary volume).

Proof

technique · direct
1.1L1L3givenchoose

Fix ε>0 and x0∈Rn. Choose R>0 with supp⁡φε⊆B‾R(0) and put K=B‾R+1(x0). Every derivative of φε vanishes off its support. Thus, for x∈B1(x0), all translated kernel derivatives vanish when y∉K. Each derivative ∂αφε is bounded by a finite constant Cα, since it is continuous with compact support.

2.1L4L5step 1.1

For each multi-index α define Fα(x)=∫f(y)∂αφε(x−y) dy. At fixed x, the integrand is Lebesgue measurable by [L4], because f is measurable and the translated kernel derivative is continuous. On B1(x0) its absolute value is bounded by Cα∣f∣1K, which is integrable by local integrability. Consequently every Fα is well-defined. If xm→x in B1(x0), continuity of the kernel gives pointwise convergence of the integrands; [L5] with this same majorant gives Fα(xm)→Fα(x). Thus every Fα is continuous locally, hence globally since x0 was arbitrary.

3.1L2L4step 1.1step 2.1

Fix x∈B1/2(x0) and a coordinate j. For ∣t∣<1/2, the integrand G(y,t)=f(y)∂αφε(x+tej−y) is integrable, differentiable in t, and has measurable derivative. The derivative is bounded by Cα+ej∣f∣1K on this interval. Therefore [L2] yields ∂jFα(x)=Fα+ej(x). This identity holds for every α,j,x.

4.1L3step 2.1step 3.1∎

Since F0=f∗φε, repeated use of step 3.1 gives every ordered iterated derivative of F0 as the integral of f against the corresponding derivative of the smooth kernel. All these integrals are continuous by step 2.1. Hence F0∈C∞ by [L3], and in particular ∂αF0=Fα=f∗(∂αφε) for every multi-index α.

Depends on

Used by

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