Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)
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.

Gaussian smoothing of finite measures

Statement

Assume AC. Let μ be a finite complex Borel measure of finite variation on Rn, n1. For t>0 define ht(x)=kt(xy)dμ(y) using the Gaussian kernel. Then htL1, ht1μ(Rn), and h^t=k^tμ^. For every complex φCc(Rn), φ(x)ht(x)dxφdμ.

Facts & Assumptions

[F1]

Under AC a finite complex measure absolutely continuous with respect to a sigma-finite positive measure has an integrable density (A finite complex measure absolutely continuous with respect to a sigma-finite positive measure has an integrable complex density).

[F3]
[F5]

Gaussian kernels have mass and norm one and the stated Gaussian transform (Gaussian summability kernels).

[F6]

Gaussian approximate identities converge uniformly on complex C0 (Complex translation, convolution, approximate identities, and mollification).

[F7]

Translation has transform multiplier e2πiyξ (Translation, modulation, linear dilation and reflection laws).

Proof

1.1

Put v=μ. The inequality μ(E)v(E) gives μv; v is finite, hence sigma-finite. F1 gives μ=uv with uL1(v), and F2 gives v(E)=Eudv, in particular udv=v(Rn). For any bounded measurable H, Hdμ=Hudv: first verify this for simple H using the density formula on sets, then approximate bounded H uniformly by quantizing its real and imaginary values. F3 bounds the error on the left by v(Rn)HHm, and the right error by u1HHm. AC enters F1 through the signed RN/Hahn/Jordan existence selections; it also covers the existence assumption omitted in the older F2 proof.

F1F2F3given
2.1

Consequently ht(x)=kt(xy)u(y)dv(y), absolutely at every x because k_t is bounded and u integrable. The joint function is Borel measurable. By F4, F5 and translation invariance, its double absolute integral is u(y)[kt(xy)dx]dv(y)=v(Rn). Fubini therefore supplies a measurable integrable h_t and its stated norm bound. With the additional modulus-one Fourier factor the same double bound applies. F4 and F7 give h^t(ξ)=k^t(ξ)e2πiyξu(y)dv(y)=k^t(ξ)μ^(ξ) by step 1.1.

F4F5F7step 1.1
3.1

For a compactly supported continuous φ, the double absolute integral after multiplication by φ(x) is at most φv(Rn). F4 exchanges the integrals. Since k_t is even, the inner test integral is (ktφ)(y), and F6 gives uniform convergence to φ(y). Thus the difference from φudv has modulus at most ktφφuL1(v)0. Step 1.1 identifies the limit with φdμ.

F4F5F6step 1.1step 2.1

Depends on

Used by

Dependency tree · two levels

70 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