Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (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 Ω⊂Rn, n≥2, be a bounded C1 domain, 1≤p<∞, and let u∈W1,p(Ω;K) admit a representative u~∈C(Ω‾;K). Then, with T the trace operator of The Lp trace operator on a bounded C1 domain, Tu=u~∣∂Ωin Lp(∂Ω); in particular Tu=0 whenever such a representative vanishes on ∂Ω. Two representatives continuous on Ω‾ of the same class have the same restriction to ∂Ω.

Facts & Assumptions

Given: The Axiom of Choice; a bounded C1 domain Ω; 1≤p<∞; a class u∈W1,p(Ω;K) and a representative u~∈C(Ω‾;K); and the trace operator T of The Lp trace operator on a bounded C1 domain.

[F1]

T:W1,p(Ω)→Lp(∂Ω) is the unique bounded linear operator with Tu=u∣∂Ω for every u∈C(Ω‾)∩W1,p(Ω), where Lp(∂Ω) uses the chart-independent surface measure of Surface integration on compact C1 hypersurfaces. (The Lp trace operator on a bounded C1 domain)

[F2]

Membership in W1,p(Ω) is a property of the Lp 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 Lp(μ) as the quotient by null functions)

[F3]

If two continuous functions on an open set Ω⊆Rn agree almost everywhere, they agree everywhere: the disagreement set is open, and a nonempty open subset of Rn contains a nondegenerate box, which has positive Lebesgue measure by the box formula. (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included)

[F4]

Every point of the topological boundary ∂Ω of an open set Ω is the limit of a sequence in Ω; hence a function continuous on Ω‾ is determined on ∂Ω by its values on Ω.

Proof

technique · direct
1.1F1F2algebragiven

The trace is the classical restriction. The representative u~ lies in C(Ω‾)∩W1,p(Ω): its class is the class of u, so it is an element of W1,p(Ω) in the quotient sense, and it is continuous on the compact set Ω‾ by hypothesis. By the defining property of T in [F1], Tu=u~∣∂Ω in Lp(∂Ω).

1.2F3F4algebra

Continuous representatives are unique on ∂Ω. Let u~,v~∈C(Ω‾) represent the same class. Then u~=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∈∂Ω take xm∈Ω with xm→x by [F4]; then u~(x)=lim⁡mu~(xm)=lim⁡mv~(xm)=v~(x) by continuity of both functions on Ω‾. Hence the restrictions to ∂Ω coincide.

2.1step 1.1step 1.2algebragiven∎

Conclusion. Step 1.1 gives Tu=u~∣∂Ω; if u~ vanishes on ∂Ω then Tu=0 in Lp(∂Ω), 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 Tf=f∣∂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.

Depends on

Used by

Dependency tree · two levels

48 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