LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-09-08 (Codex)

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 Euclidean bump for a compact set inside an open set

Statement

If $K \subseteq U \subseteq R^{n}$ with $K$ compact and $U$ open, then there exists a smooth function $ρ : R^{n} \to [0, 1]$ such that $ρ = 1$ on $K$ and $supp (ρ) \subseteq U$ .

Facts & Assumptions

Given: A compact set $K \subseteq R^{n}$ and an open set $U \supseteq K$ .

[L1]

Compactness gives a finite subcover from an indexed ambient open cover (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, claim 3).

[L2]

The explicit concentric-ball construction gives a smooth function into $[0, 1]$ , equal to $1$ on the inner closed ball and supported inside the outer open ball (A smooth bump between concentric Euclidean balls).

[L3]

The one-variable sum and product rules apply to coordinate derivatives (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$ ). Smoothness requires all iterated coordinate derivatives to exist and be continuous ( $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[F1]

Support is the closure of the nonzero locus (The support of a function on $R^{n}$ and its compactly supported Riemann integral).

Proof

technique · direct

1.1givenF1construct

If $K = \emptyset$ , the zero function has empty support and satisfies the claim. Suppose henceforth that $K \neq \emptyset$ . Consider all triples $(p, r, R)$ with $p \in K$ , $0 < r < R$ , and $B_{R} (p) \subseteq U$ . Their inner balls $B_{r} (p)$ form an indexed open cover of $K$ : openness gives a ball $B_{R} (p) \subseteq U$ at each $p$ , and $r = R / 2$ is admissible. This defines the whole family without making a simultaneous choice at every point.

2.1L1L2step 1.1

By [L1], finitely many admissible triples $(p_{i}, r_{i}, R_{i})$ , $1 \leq i \leq m$ , have inner balls covering $K$ . For each of these finitely many triples use the explicit formula in [L2], with $x$ replaced by $x - p_{i}$ , to define $ρ_{i}$ . Translation preserves the coordinate-derivative formulas, so each $ρ_{i}$ is smooth, lies in $[0, 1]$ , equals $1$ on ${\overline{B}}_{r_{i}} (p_{i})$ , and has support contained in $B_{R_{i}} (p_{i}) \subseteq U$ .

3.1L3step 2.1construct

Define $ρ = 1 - \prod_{i = 1}^{m} (1 - ρ_{i})$ . Repeated use of [L3] shows that each iterated coordinate derivative is a finite sum of products of continuous derivatives of the $ρ_{i}$ , so $ρ$ is smooth. Since every factor lies in $[0, 1]$ , so does $ρ$ . On each inner ball one factor is zero; hence $ρ = 1$ on their union, an open neighbourhood of $K$ .

4.1F1step 2.1step 3.1construct

Let $F = ⋃_{i = 1}^{m} supp ρ_{i}$ . Each support is closed by [F1], so the finite union $F$ is closed, and step 2.1 gives $F \subseteq U$ . Off $F$ , every $ρ_{i}$ vanishes, so the formula in step 3.1 gives $ρ = 0$ . Therefore the closure of the nonzero locus of $ρ$ lies in $F$ : $supp ρ \subseteq F \subseteq U$ .

5.1step 1.1step 3.1step 4.1∎

Steps 3.1 and 4.1 give all three required properties; step 1.1 handled the empty case.

Depends on

Used by

Boundary H² regularity needs domain regularity Counterexample
Critical traces fail compactness under boundary dilation Counterexample
Morrey--Rellich compactness loses the endpoint H"older exponent Counterexample
Outward dilation defeats subcritical inclusion and homogeneous Poincare on Euclidean space Counterexample
Rellich compactness fails on ℝⁿ by translations Counterexample
Smooth interior data do not repair incompatible Dirichlet corner values Counterexample
The W^1,p→ L^q bound fails for q>p^* by dilation Counterexample
W^1,n is not contained in L^∞ Counterexample
Absolute value has a Dirac second derivative Example
Dirichlet Laplacian eigenpairs on an interval Example
Translation and differentiation symbols Example
A chart bump at a point with prescribed support Lemma
A metric-gradient critical crossing preserves the pointed disk pair Lemma
Bessel potentials shift Sobolev order Lemma
Compactified unstable manifolds give the Morse--Smale CW decomposition Lemma
Finite chart localization of compactly supported top forms, including boundary Lemma
Increasing reparametrization of finitely many critical levels Lemma
Mean-zero Poincare estimate on bounded connected extension domains below the dimension Lemma
Moving a sphere off a lower-dimensional submanifold Lemma
Smooth compactly supported functions of an open set are dense in L² Lemma
The cutoff difference-quotient commutator estimate Lemma
The velocity field of an isotopy extends to a neighbourhood Lemma
Uniformly bounded difference quotients represent a weak derivative Lemma
Vanishing-viscosity families are locally precompact in L¹ Lemma
Connection laws in directional form Proposition
Compactness of W^1,p(Ω)↪ Lᵖ(Ω) on bounded extension domains Theorem
Existence of bounded Kruzhkov entropy solutions Theorem
Higher-order Rellich--Kondrachov compactness Theorem
Higher-order Sobolev embedding Theorem
Interior H² regularity for divergence-form equations Theorem
Local L¹ contraction for two entropy solutions Theorem
Morrey--Rellich compactness for p>n Theorem
Smooth partitions of unity exist on manifolds with boundary Theorem
The critical Sobolev embedding into every finite L^q Theorem
The Gagliardo-Nirenberg-Sobolev inequality for 1<p<n Theorem
The Whitney move removes a cancelling pair of intersection points Theorem

Dependency tree · two levels

32 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

John M. Lee, Introduction to Smooth Manifolds (standard reference, not scraped)
Will J. Merry, Differential Geometry (standard reference, not scraped)
Nigel Hitchin, Differentiable Manifolds (standard reference, not scraped)