LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)verified 2026-10-03 (gpt-6.1-sol)

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.

The trace agrees with classical restriction for continuous Sobolev functions

Statement

Assume the Axiom of Choice. Let $Ω \subset R^{n}$ , $n \geq 2$ , be a bounded $C^{1}$ domain, $1 \leq p < \infty$ , and let $u \in W^{1, p} (Ω; K)$ admit a representative $\tilde{u} \in C (\overline{Ω}; K)$ . Then, with $T$ the trace operator of The $L^{p}$ trace operator on a bounded $C^{1}$ domain, $T u = \tilde{u} ∣_{\partial Ω} in L^{p} (\partial Ω);$ in particular $T u = 0$ whenever such a representative vanishes on $\partial Ω$ . Two representatives continuous on $\overline{Ω}$ of the same class have the same restriction to $\partial Ω$ .

Facts & Assumptions

Given: The Axiom of Choice; a bounded $C^{1}$ domain $Ω$ ; $1 \leq p < \infty$ ; a class $u \in W^{1, p} (Ω; K)$ and a representative $\tilde{u} \in C (\overline{Ω}; K)$ ; and the trace operator $T$ of The $L^{p}$ trace operator on a bounded $C^{1}$ domain.

[F1]

$T : W^{1, p} (Ω) \to L^{p} (\partial Ω)$ is the unique bounded linear operator with $T u = u ∣_{\partial Ω}$ for every $u \in C (\overline{Ω}) \cap W^{1, p} (Ω)$ , where $L^{p} (\partial Ω)$ uses the chart-independent surface measure of Surface integration on compact C1 hypersurfaces. (The $L^{p}$ trace operator on a bounded $C^{1}$ domain)

[F2]

Membership in $W^{1, p} (Ω)$ is a property of the $L^{p}$ class: a representative differing on a null set defines the same class and the same weak derivatives, and classes are almost-everywhere classes. (Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions)

[F3]

If two continuous functions on an open set $Ω \subseteq R^{n}$ agree almost everywhere, they agree everywhere: the disagreement set is open, and a nonempty open subset of $R^{n}$ contains a nondegenerate box, which has positive Lebesgue measure by the box formula. (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)

[F4]

Every point of the topological boundary $\partial Ω$ of an open set $Ω$ is the limit of a sequence in $Ω$ ; hence a function continuous on $\overline{Ω}$ is determined on $\partial Ω$ by its values on $Ω$ .

Proof

technique · direct

1.1F1F2algebragiven

The trace is the classical restriction. The representative $\tilde{u}$ lies in $C (\overline{Ω}) \cap W^{1, p} (Ω)$ : its class is the class of $u$ , so it is an element of $W^{1, p} (Ω)$ in the quotient sense, and it is continuous on the compact set $\overline{Ω}$ by hypothesis. By the defining property of $T$ in [F1], $T u = \tilde{u} ∣_{\partial Ω}$ in $L^{p} (\partial Ω)$ .

1.2F3F4algebra

Continuous representatives are unique on $\partial Ω$ . Let $\tilde{u}, \tilde{v} \in C (\overline{Ω})$ represent the same class. Then $\tilde{u} = \tilde{v}$ almost everywhere on $Ω$ , so by [F3] they agree everywhere on $Ω$ (the disagreement set, if nonempty, would be a nonempty open subset of $Ω$ and would have positive measure). For $x \in \partial Ω$ take $x_{m} \in Ω$ with $x_{m} \to x$ by [F4]; then $\tilde{u} (x) = \lim_{m} \tilde{u} (x_{m}) = \lim_{m} \tilde{v} (x_{m}) = \tilde{v} (x)$ by continuity of both functions on $\overline{Ω}$ . Hence the restrictions to $\partial Ω$ coincide.

2.1step 1.1step 1.2algebragiven∎

Conclusion. Step 1.1 gives $T u = \tilde{u} ∣_{\partial Ω}$ ; if $\tilde{u}$ vanishes on $\partial Ω$ then $T u = 0$ in $L^{p} (\partial Ω)$ , and step 1.2 shows that two such continuous representatives have the same boundary restriction, so the identity is independent of the choice of continuous representative.

Source notes

Teschl's Theorem 9.18 (printed p. 209) states $T f = f ∣_{\partial U}$ for continuous functions; Laugesen's opening clause and Step 4 of Theorem 3.14 (printed pp. 62-64) and Schikorra's Theorem III.3.21(1) (printed p. 76) record the same agreement. The lemma above is the formal unpacking of the defining clause of the trace operator together with the elementary uniqueness of a continuous representative on the boundary.

The trace agrees with classical restriction for continuous Sobolev functions

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources