LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Euclidean spaces admit a smooth compactly supported unit-mass bump

Statement

Assume Countable Choice. For every integer $d \geq 1$ there is a nonnegative function $ρ_{d} : R^{d} \to R$ with continuous partial derivatives of every order, support exactly $[- 1, 1]^{d}$ , strictly positive on $(- 1, 1)^{d}$ , and Lebesgue integral $\int_{R^{d}} ρ_{d} (x) d x = 1$ . Here the support is the closure of the set where the function is nonzero.

Statement references

The Axiom of Countable Choice ( ${A C}_{ω}$ )

J. K. Hunter, MIT 18.102, Chapter 4, §9 Convolution, Lemma 58

Facts & Assumptions

Given: Countable Choice and an integer $d \geq 1$ .

[A1]

Countable Choice is assumed in the product-Lebesgue identification used in [F4]. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

For every integer $N \geq 0$ , $u^{N} e^{- u} \to 0$ as $u \to + \infty$ ; therefore a polynomial in $u$ times $e^{- u}$ tends to zero. The exponential dominates every fixed nonnegative integer power at $+ \infty$

[F2]

The exponential is smooth and positive, and the chain and product rules differentiate its affine composites and finite products. The exponential function is smooth and $(\exp)^{'} = \exp$ The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$

[F3]

Under Countable Choice, the Lebesgue measure of a box is its side-length product; a continuous function on a compact interval is bounded, and the nonnegative integral is monotone and homogeneous. A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value Monotonicity and nonnegative homogeneity of the nonnegative integral The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F4]

Under Countable Choice, Euclidean Lebesgue measure on a finite product is the product of the coordinate Lebesgue measures, and Tonelli factors nonnegative product integrals. On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n} Tonelli's theorem for nonnegative measurable functions on a sigma-finite product The Axiom of Countable Choice ( ${A C}_{ω}$ )

Proof

1.1F1F2giveninduction

Define $ϕ (t) = e^{- 1 / t}$ for $t > 0$ and $ϕ (t) = 0$ for $t \leq 0$ . For each $k \geq 0$ , repeated chain and product rules give $ϕ^{(k)} (t) = P_{k} (1 / t) e^{- 1 / t}$ on $t > 0$ for a polynomial $P_{k}$ : it holds with $P_{0} = 1$ , and if $u = 1 / t$ then differentiation replaces $P_{k} (u)$ by the polynomial $u^{2} (P_{k} (u) - P_{k}^{'} (u))$ . By [F1], this derivative tends to $0$ as $t ↓ 0$ . Its difference quotient at $0$ is $u P_{k} (u) e^{- u}$ with $u = 1 / t$ , which also tends to $0$ by [F1]; from the left it is zero. Induction therefore gives every derivative at $0$ equal to $0$ and continuous there, so $ϕ$ is smooth on $R$ .

2.1A1F2F3step 1.1

Set $Φ (t) = ϕ (t + 1) ϕ (1 - t)$ . By [F2], $Φ$ is smooth. It vanishes for $t \notin [- 1, 1]$ and is positive for $- 1 < t < 1$ , so its support is $[- 1, 1]$ . Let $I = \int_{R} Φ (t) d t$ . The extreme-value bound [F3] makes $Φ$ bounded on $[- 1, 1]$ , so $I < \infty$ . Since $Φ (0) = e^{- 2} > 0$ , continuity gives $δ \in (0, 1)$ with $Φ (t) \geq e^{- 2} / 2$ on $[- δ, δ]$ ; [F3] gives $I \geq δ e^{- 2} > 0$ . Hence $ψ = Φ / I$ is smooth, supported on $[- 1, 1]$ , positive on $(- 1, 1)$ , and has integral one.

3.1F2givenstep 2.1

Define $ρ_{d} (x_{1}, \dots, x_{d}) = \prod_{j = 1}^{d} ψ (x_{j})$ . Repeated coordinatewise chain and product rules give every partial derivative as $\prod_{j = 1}^{d} ψ^{(α_{j})} (x_{j})$ for its multi-index $α$ , so all partial derivatives are continuous. The function is nonnegative, vanishes outside $[- 1, 1]^{d}$ , and is positive at every point of $(- 1, 1)^{d}$ ; therefore its support is exactly that closed cube.

4.1A1F4step 2.1step 3.1induction∎

For $d = 1$ , $\int ρ_{1} = 1$ by step 2.1. By step 3.1, $ρ_{d}$ is a nonnegative Borel function supported in the compact cube. For $d \geq 2$ , split $R^{d} = R^{d - 1} \times R$ . By [F4] and Tonelli, $\int ρ_{d} d x = (\int ρ_{d - 1} d x) (\int ψ d t)$ ; the second factor is $1$ by step 2.1. Induction on $d$ proves $\int_{R^{d}} ρ_{d} d x = 1$ .

Depends on

Used by

Dependency tree · two levels

76 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

MIT 18.102, Chapter 4, §9 Convolution, Lemma 58, printed pp. 136–137 (standard reference, not scraped)