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 summability kernels

Statement

Assume countable choice. For $t > 0$ put $k_{t} (x) = t^{- n / 2} e^{- π ∣ x ∣^{2} / t}$ on $R^{n}$ , $n \geq 1$ . Then $k_{t} \geq 0$ , $\int k_{t} = ∥ k_{t} ∥_{1} = 1$ , $\hat{k_{t}} (ξ) = e^{- π t ∣ ξ ∣^{2}}$ , and $(k_{t})_{t > 0}$ is an $L^{1}$ approximate identity as $t ↓ 0$ . Directly, $k_{t} (z) = \int e^{- π t ∣ ξ ∣^{2}} e^{2 π i z \cdot ξ} d ξ .$

Facts & Assumptions

Given: $n \geq 1$ , $t > 0$ and The Axiom of Countable Choice ( ${A C}_{ω}$ ).

[F1]

The Gaussian transform is $F (e^{- π s ∣ x ∣^{2}}) (ξ) = s^{- n / 2} e^{- π ∣ ξ ∣^{2} / s}$ for $s > 0$ (Euclidean Gaussian transform with the 2π normalization).

[F2]

The complex Lebesgue substitution formula uses the absolute Jacobian (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

[F3]

Dominated convergence passes integrable tails to zero (Dominated convergence).

[F4]

An approximate identity has unit mass, uniformly bounded $L^{1}$ norm and vanishing absolute tails outside every fixed radius (An $L^{1}$ approximate identity on $R^{n}$ ).

Proof

1.1

Apply F1 with $s = 1 / t$ and multiply by $t^{- n / 2}$ to obtain $\hat{k_{t}} (ξ) = e^{- π t ∣ ξ ∣^{2}}$ . At $ξ = 0$ this gives mass one; positivity gives the same $L^{1}$ norm. Applying F1 with $s = t$ at frequency $- z$ proves the displayed inverse integral without an inversion theorem.

F1given

2.1

Write $y = x / \sqrt{t}$ . F2 gives $\int_{∣ x ∣ > δ} k_{t} (x) d x = \int_{∣ y ∣ > δ / \sqrt{t}} e^{- π ∣ y ∣^{2}} d y$ . This tends to zero: F3 applied to the explicit integer-radius tails with majorant the integrable Gaussian gives their convergence to zero, and monotonicity bounds every sufficiently small t-tail by any fixed integer tail. All three conditions in F4 now hold with norm bound one. Countable choice is inherited from the Gaussian and substitution results.

F1F2F3F4step 1.1∎

Depends on

Used by

Gaussian smoothing of finite measures Lemma
Gaussian Fourier summability at Lebesgue points Theorem

Dependency tree · two levels

43 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

Gerald Teschl, Topics in Real and Functional Analysis (2017) (standard reference, not scraped)