LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

Fixed support test function spaces are complete

Statement

For every compact $K \subseteq Ω$ with $Ω \subseteq R^{n}$ open, the space $D_{K}$ is Hausdorff, locally convex and complete for $d (f, g) = \sum_{m = 0}^{\infty} 2^{- m - 1} \min (1, p_{m} (f - g)) .$ This metric induces exactly its derivative-seminorm topology. Multiplying the metric by two gives the equivalent convention with weights $2^{- m}$ . These assertions require no choice axiom.

Facts & Assumptions

[F1]

The functions, increasing seminorms and zero extensions are defined in Fixed support test function frechet space.

[F2]

On a nondegenerate closed real interval, uniform convergence of continuously differentiable functions and their derivatives identifies the derivative of the limit; the weaker hypothesis of convergence at one point suffices (If continuously differentiable functions converge at one point and their derivatives converge uniformly on a closed interval, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit). Apply this to real and imaginary parts separately.

Proof

Given: a compact $K$ and its space in F1.

1.1

Nonnegativity, symmetry and separation for $d$ follow from F1 and its $p_{0}$ term. The inequality $\min (1, a + b) \leq \min (1, a) + \min (1, b)$ gives the triangle inequality term by term. For fixed $m$ and $0 < ε < 1$ , $d (f, g) < 2^{- m - 1} ε$ implies $p_{m} (f - g) < ε$ . Conversely, given $ε > 0$ , choose $M$ with $\sum_{m > M} 2^{- m - 1} < ε / 2$ ; then $p_{M} (f - g) < ε / 2$ gives $d (f, g) < ε$ . These bounds identify the two topologies and their Cauchy sequences. Seminorm balls are convex, and their triangle and homogeneity inequalities give continuity of vector operations.

givenF1algebra

2.1

Let $(f_{j})$ be $d$ -Cauchy and extend each function smoothly by zero to $R^{n}$ . For every multi-index $α$ , the functions $\partial^{α} f_{j}$ are uniformly Cauchy on all of $R^{n}$ : outside $K$ they vanish and on $K$ the bound is $p_{∣ α ∣} (f_{j} - f_{k})$ . At each point their complex values have a unique limit $g_{α} (x)$ . Passing $k$ to infinity in the uniform Cauchy bound proves uniform convergence to $g_{α}$ . This definition uses unique limits, not a choice of subsequences. Each $g_{α}$ is continuous: at a point, approximate it uniformly by one continuous derivative within $ε / 3$ and use continuity of that derivative. It vanishes off $K$ .

step 1.1F1

3.1

Fix a coordinate direction $e_{i}$ , a point $x$ and a positive $h$ . On $[- h, h]$ , the functions $t \mapsto \partial^{α} f_{j} (x + t e_{i})$ and their derivatives converge uniformly to $g_{α} (x + t e_{i})$ and $g_{α + e_{i}} (x + t e_{i})$ respectively. F2, componentwise, gives $\partial_{i} g_{α} (x) = g_{α + e_{i}} (x)$ . All these functions are continuous by step 2.1, so iterating this identity shows $g_{0}$ is smooth with every derivative $g_{α}$ . Its support is contained in the closed set $K$ , hence $g_{0} ∣_{Ω} \in D_{K}$ .

step 2.1F2

4.1

Uniform convergence of the finitely many derivatives of order at most $m$ gives $p_{m} (f_{j} - g_{0}) \to 0$ for each $m$ , hence $d (f_{j}, g_{0}) \to 0$ by step 1.1. This proves completeness. If $K$ is empty or has empty interior, F1 makes the space zero and the same argument yields its sole element. No endpoint differentiation in $Ω$ was assumed: the coordinate segments in step 3.1 lie in the globally smooth zero extension. $□$

step 3.1step 2.1step 1.1F1

Depends on

Used by

Cited to discharge well-definedness by Fixed support test function frechet space.

Dependency tree · two levels

22 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 (2022) (standard reference, not scraped)