LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

Zero extension of W_0^{1,p} has no boundary derivative

Statement

Assume Countable Choice. For any open $Ω \subseteq R^{n}$ , $n \geq 1$ , any $1 \leq p \leq \infty$ and any $K \in {R, C}$ , extension by zero $E_{0} u (x) = u (x) (x \in Ω), E_{0} u (x) = 0 (x \notin Ω),$ acted on representatives, sends $W_{0}^{1, p} (Ω; K)$ linearly into $W^{1, p} (R^{n}; K)$ . For every $u \in W_{0}^{1, p} (Ω; K)$ and every coordinate direction $i$ , the class $D_{i} (E_{0} u)$ is the zero extension of the class $D_{i} u$ , and every $L^{p}$ component norm is preserved: $∥ E_{0} u ∥_{L^{p} (R^{n})} = ∥ u ∥_{L^{p} (Ω)}, ∥ D_{i} (E_{0} u) ∥_{L^{p} (R^{n})} = ∥ D_{i} u ∥_{L^{p} (Ω)},$ so that $∥ E_{0} u ∥_{W^{1, p} (R^{n})} = ∥ u ∥_{W^{1, p} (Ω)}$ .

Facts & Assumptions

Given: Countable Choice; an open set $Ω \subseteq R^{n}$ with $n \geq 1$ ; $1 \leq p \leq \infty$ ; $K \in {R, C}$ ; a class $u \in W_{0}^{1, p} (Ω; K)$ ; and a test function $φ \in C_{c}^{\infty} (R^{n})$ .

[F1]

Membership $u \in W_{0}^{1, p} (Ω; K)$ means that for every $δ > 0$ there is $ψ \in C_{c}^{\infty} (Ω; K)$ with $∥ u - ψ ∥_{W^{1, p} (Ω)} < δ$ , and $W_{0}^{1, p} \subseteq W^{1, p}$ ; the norm is the Sobolev norm of Integer-order Sobolev spaces and their norms (Zero-boundary Sobolev space as a norm closure).

[F2]

For $w \in L^{p} (Ω; K)$ and its zero extension $E_{0} w$ : the extension is measurable, $∣ E_{0} w ∣ = ∣ w ∣$ on $Ω$ and $E_{0} w = 0$ off $Ω$ , so $∥ E_{0} w ∥_{L^{p} (R^{n})} = ∥ w ∥_{L^{p} (Ω)}$ for $1 \leq p \leq \infty$ because the integral over a measurable set is the integral of the indicator product; the map $E_{0}$ is linear on classes; and for $v \in C_{c}^{\infty} (Ω; K)$ the extension $E_{0} v$ lies in $C_{c}^{\infty} (R^{n})$ with $\partial_{i} (E_{0} v) = E_{0} (\partial_{i} v)$ for every $i$ (Integral over a measurable subset, Complex Lp classes and Euclidean test-function conventions).

[F3]

The defining weak identity on an open set $V$ is $\int_{V} w D^{α} ψ = (- 1)^{∣ α ∣} \int_{V} (D^{α} w) ψ$ for all $ψ \in C_{c}^{\infty} (V; K)$ (Weak derivative of a locally integrable function).

[F4]

A $C^{1}$ (indeed $C^{\infty}$ ) function on an open set has each of its classical partial derivatives as its weak derivative there (Classical derivatives agree with weak derivatives).

[F5]

Hölder's inequality: for conjugate exponents $p, q$ and measurable $f, g$ , $\int ∣ f g ∣ \leq ∥ f ∥_{p} ∥ g ∥_{q}$ whenever the norms on the right are finite (Holder's inequality for integrals, including the endpoint cases).

[F6]

A class in $W^{1, p} (R^{n}; K)$ is exactly an $L^{p}$ class whose coordinate weak derivatives exist as $L^{p}$ classes, with the norm of Integer-order Sobolev spaces and their norms; weak derivatives are unique up to null sets, and changing representatives does not change the classes (Uniqueness of a weak derivative as an almost-everywhere class, Weak differentiation ignores null-set changes).

Choice use. Countable Choice is used once, in step 1.3, to select a single test-function approximant for each precision $1 / j$ ; the rest of the argument is explicit and choice-free.

Proof

technique · direct

1.1F2given

The zero extension $E_{0}$ is linear on $L^{p}$ classes, preserves $L^{p}$ norms, and sends $C_{c}^{\infty} (Ω; K)$ into $C_{c}^{\infty} (R^{n})$ with $\partial_{i} (E_{0} v) = E_{0} (\partial_{i} v)$ ; in particular $E_{0} v_{j} - E_{0} v_{k} = E_{0} (v_{j} - v_{k})$ and $∥ E_{0} w ∥_{L^{p} (R^{n})} = ∥ w ∥_{L^{p} (Ω)}$ for every $L^{p}$ class $w$ .

1.2F2F3F4given

For $v \in C_{c}^{\infty} (Ω; K)$ the classical partial derivative $\partial_{i} (E_{0} v)$ is the weak $i$ -derivative of $E_{0} v$ on $R^{n}$ , so for every test $φ \in C_{c}^{\infty} (R^{n})$ one has $\int_{R^{n}} E_{0} v \partial_{i} φ = - \int_{R^{n}} E_{0} (\partial_{i} v) φ .$

1.3F1given

Since $u \in W_{0}^{1, p} (Ω; K)$ , [F1] with $δ = 1 / j$ provides for each integer $j \geq 1$ some $v_{j} \in C_{c}^{\infty} (Ω; K)$ with $∥ u - v_{j} ∥_{W^{1, p} (Ω)} < 1 / j$ ; Countable Choice selects one such sequence $(v_{j})_{j \geq 1}$ .

2.1F1step 1.1step 1.3

The linearity and isometry of $E_{0}$ give $E_{0} v_{j} \to E_{0} u$ and $E_{0} (\partial_{i} v_{j}) \to E_{0} (D_{i} u)$ in $L^{p} (R^{n})$ as $j \to \infty$ , because $v_{j} \to u$ and $\partial_{i} v_{j} \to D_{i} u$ in $L^{p} (Ω)$ by step 1.3 and the definition of the Sobolev norm.

3.1F5step 1.2step 2.1

For the fixed test $φ$ , step 1.2 gives $\int E_{0} v_{j} \partial_{i} φ = - \int E_{0} (\partial_{i} v_{j}) φ$ for every $j$ . Hölder's inequality on the compact support of $φ$ turns the $L^{p}$ convergences of step 2.1 into convergence of both integrals: $\int_{R^{n}} E_{0} v_{j} \partial_{i} φ \to \int_{R^{n}} E_{0} u \partial_{i} φ$ and $\int_{R^{n}} E_{0} (\partial_{i} v_{j}) φ \to \int_{R^{n}} E_{0} (D_{i} u) φ$ ; hence $\int_{R^{n}} E_{0} u \partial_{i} φ = - \int_{R^{n}} E_{0} (D_{i} u) φ .$

4.1F6step 1.1step 3.1∎

Since $φ$ was an arbitrary test function, step 3.1 exhibits $E_{0} (D_{i} u)$ as a weak $i$ -derivative of the $L^{p}$ class $E_{0} u$ on $R^{n}$ ; by [F6] therefore $E_{0} u \in W^{1, p} (R^{n}; K)$ with $D_{i} (E_{0} u) = E_{0} (D_{i} u)$ almost everywhere, the component norms agree by step 1.1, and $u \mapsto E_{0} u$ is linear because $E_{0}$ is. Changing representatives on null sets changes no class by [F6], the case $k = 0$ does not arise here, and complex scalars are covered by the same bilinear pairing.

Depends on

Used by

Boundary regularity required by the constructed extension Remark

Dependency tree · two levels

51 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

Juha Kinnunen, Sobolev Spaces (2026), Theorem 1.25 (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (2020), Theorem 3.12 (standard reference, not scraped)