LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

A fixed-support smooth test-function space is separable

Statement

Let $I = [a, b]$ with $a < b$ . Let $D_{I}$ be the real-valued smooth functions $φ : R \to R$ that vanish outside $I$ , with seminorms

$p_{M} (φ) = \max_{0 \leq j \leq M} \sup_{x \in I} ∣ φ^{(j)} (x) ∣, M \in N_{0},$

and metric

$d (φ, ψ) = \sum_{M = 0}^{\infty} 2^{- M - 1} \min (1, p_{M} (φ - ψ)) .$

Then $D_{I}$ is separable in this metric.

Statement references

Dyatlov, Lecture Notes for 18.155, fixed-support test-function spaces

Facts & Assumptions

Given: A nondegenerate compact interval $I = [a, b]$ .

[F1]

The fixed-support test-function space has the derivative seminorms and metric displayed in the Statement (Fixed support test function frechet space).

[F2]

The function $θ (t) = q (t) / (q (t) + q (1 - t))$ , where $q (t) = e^{- 1 / t}$ for $t > 0$ and $q (t) = 0$ for $t \leq 0$ , is smooth, equals zero on $t \leq 0$ , and equals one on $t \geq 1$ ; its flatness at the endpoints follows from the explicit construction (Explicit compactly supported smooth cutoffs, proof step 2.1).

[F3]

Every continuous real function on $I$ is uniformly approximated by real polynomials (Polynomials are uniformly dense in $C ([a, b], R)$ for every closed interval).

[F4]

Taylor's formula with a Lagrange remainder bounds a smooth function whose first $N$ endpoint derivatives vanish by a constant times the $N$ th power of the distance to that endpoint (Taylor's Lagrange remainder follows from repeated Rolle steps).

[F5]

For a continuously differentiable real function on an interval, the integral of its derivative equals the endpoint difference (The fundamental theorem of calculus and integration by parts).

[F6]

For every $ε > 0$ there is an integer $n \geq 1$ with $1 / n < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[F7]

A continuous real function on a compact interval is bounded (Continuous functions on a closed interval attain their extrema); the chain and product rules hold (Sum, product, quotient, and chain rules from difference quotients).

[F8]

The natural numbers are unbounded in $R$ , so integers $n$ above the fixed cutoff can tend to infinity (Every complete ordered field is Archimedean).

Proof

1.1givenF1F2F4F6F7F8algebra

For each integer $n > 2 / (b - a)$ define $χ_{n} (x) = θ (n (x - a)) θ (n (b - x))$ ; such integers exist by [F6], and can tend to infinity by [F8]. By [F2], $χ_{n}$ is smooth, vanishes off $I$ , and equals one on $[a + 1 / n, b - 1 / n]$ . Every derivative of $θ$ is continuous and vanishes outside $[0, 1]$ in positive order, so [F7] bounds it on $[0, 1]$ ; repeated chain and product rules [F7] bound $χ_{n}^{(j)}$ by a constant times $n^{j}$ . For every $φ \in D_{I}$ , all derivatives of its zero extension vanish at $a$ and $b$ . Fix $M$ . Taylor's formula [F4] gives, for every $N \geq 1$ and each $0 \leq r \leq M$ , bounds $∣ φ^{(r)} (x) ∣ \leq C_{r, N} ∣ x - a ∣^{N}$ near $a$ and $∣ φ^{(r)} (x) ∣ \leq C_{r, N}^{'} ∣ b - x ∣^{N}$ near $b$ . Applying the product rule on the two boundary strips, and taking $N > M$ , shows $p_{M} (φ - χ_{n} φ) \to 0$ .

1.2F2F3F5algebrachoose

Fix $n$ and $M$ . By [F3], choose a real polynomial $p$ uniformly approximating $φ^{(M)}$ on $I$ , and integrate it $M$ times while matching the values $φ^{(j)} (a)$ for $0 \leq j < M$ to obtain a polynomial $q_{0}$ . Put $e = φ - q_{0}$ . Then $e^{(M)} = φ^{(M)} - p$ and $e^{(j)} (a) = 0$ for $j < M$ . Repeated application of [F5], inducting downward from $j = M - 1$ , gives $\sup_{I} ∣ e^{(j)} ∣ \leq (b - a)^{M - j} \sup_{I} ∣ e^{(M)} ∣ (0 \leq j < M);$ for $j = M$ the error is just $\sup_{I} ∣ e^{(M)} ∣$ . Thus sufficiently accurate approximation at order $M$ makes every derivative through order $M$ uniformly close. Approximating the finitely many coefficients of $q_{0}$ by rational numbers gives $q \in Q [x]$ with the same approximation to any prescribed tolerance. Since the finitely many derivatives of $χ_{n}$ are bounded on $I$ , the product rule makes $p_{M} (χ_{n} (q - φ))$ arbitrarily small. Thus $χ_{n} q \in D_{I}$ approximates $χ_{n} φ$ in $p_{M}$ .

2.1step 1.1step 1.2F1choose∎

The set ${χ_{n} q : n \in N, n > 2 / (b - a), q \in Q [x]}$ is countable. Given a metric neighborhood of $φ \in D_{I}$ , the summable metric weights reduce it to finitely many seminorms, bounded by $p_{M}$ for the largest index. Choose $n$ in step 1.1 so that $p_{M} (φ - χ_{n} φ)$ is less than half the target tolerance, then choose $q$ in step 1.2 so that $p_{M} (χ_{n} φ - χ_{n} q)$ is less than the other half. The triangle inequality places $χ_{n} q$ in the neighborhood. Hence this countable set is dense.

Depends on

Used by

Polynomial activation convolutions have a common degree bound Lemma

Dependency tree · two levels

34 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

Semyon Dyatlov, Lecture Notes for 18.155, fixed-support test-function topology (standard reference, not scraped)