ExampleConstruction: Literature-sourcedVerification: 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 of an affine function on a ball is its classical restriction

Example

Assume the Axiom of Choice. Let $Ω = B_{R} (0) \subset R^{n}$ , $n \geq 2$ , $1 \leq p < \infty$ , $c \in R^{n}$ , $d \in K$ , and $u (x) = c \cdot x + d$ . Then $u \in C^{\infty} (\overline{Ω}) \cap W^{1, p} (Ω)$ and, by The trace agrees with classical restriction for continuous Sobolev functions, $T u = (c \cdot x + d) ∣_{\partial Ω};$ moreover $T u \in W^{1 - 1 / p, p} (\partial Ω)$ for $1 < p < \infty$ with $∥ T u ∥_{W^{1 - 1 / p, p} (\partial Ω)} \leq C (R, n, p) (∣ c ∣ R + ∣ d ∣)$ by The sharp trace theorem: boundedness and range in the fractional space. At $p = 1$ only the $L^{1}$ statement is made; the space is not renamed $W^{0, 1} (\partial Ω)$ . On the sphere $\partial B_{R} (0)$ the boundary $L^{p}$ norm is the classical surface integral $∥ T u ∥_{L^{p} (\partial Ω)}^{p} = R^{n - 1} \int_{S^{n - 1}} ∣ c \cdot R ω + d ∣^{p} d σ (ω),$ with $σ$ the surface measure on the unit sphere.

Facts & Assumptions

Given: The Axiom of Choice; $n \geq 2$ , $R > 0$ , $1 \leq p < \infty$ , $c \in R^{n}$ , $d \in K$ ; the affine function $u (x) = c \cdot x + d$ ; and the trace $T$ of The $L^{p}$ trace operator on a bounded $C^{1}$ domain.

[F1]

If a $W^{1, p} (Ω)$ class has a continuous representative on $\overline{Ω}$ , its trace is the classical restriction of that representative. (The trace agrees with classical restriction for continuous Sobolev functions)

[F2]

For $1 < p < \infty$ the trace maps $W^{1, p} (Ω)$ onto $W^{θ, p} (\partial Ω)$ with $θ = 1 - 1 / p$ and is bounded: $∥ T u ∥_{W^{θ, p} (\partial Ω)} \leq C (Ω, p) ∥ u ∥_{W^{1, p} (Ω)}$ . (The sharp trace theorem: boundedness and range in the fractional space, The fractional Sobolev space on a compact $C^{1}$ boundary)

[F3]

The surface integral on the sphere is $\int_{\partial B_{R} (0)} h d S = R^{n - 1} \int_{S^{n - 1}} h (R ω) d σ (ω)$ , and the boundary integral is finite for continuous $h$ on the compact boundary. (Surface integration on compact C1 hypersurfaces)

[F4]

The Euclidean ball has finite Lebesgue measure, and $\int_{B_{R} (0)} ∣ x ∣^{p} d x \leq R^{p} ∣ B_{R} (0) ∣$ . (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)

Verification

1.1F1F4algebragiven

The trace is the classical restriction, with a controlled norm. The affine function is smooth on $\overline{Ω}$ ; its gradient is the constant $c$ , so $\int_{Ω} ∣ u ∣^{p} d x \leq 2^{p - 1} (∣ c ∣^{p} \int_{Ω} ∣ x ∣^{p} d x + ∣ d ∣^{p} ∣ Ω ∣) \leq C (R, n, p) (∣ c ∣ R + ∣ d ∣)^{p}$ and $\int_{Ω} ∣ \partial_{i} u ∣^{p} d x = ∣ c_{i} ∣^{p} ∣ Ω ∣ \leq C (R, n, p) (∣ c ∣ R + ∣ d ∣)^{p}$ by [F4]. Hence $u \in W^{1, p} (Ω)$ with $∥ u ∥_{W^{1, p} (Ω)} \leq C^{'} (R, n, p) (∣ c ∣ R + ∣ d ∣)$ , and $u \in C (\overline{Ω})$ , so $T u = (c \cdot x + d) ∣_{\partial Ω}$ by [F1].

2.1F2F3step 1.1algebra

Fractional membership and the boundary norm. For $1 < p < \infty$ put $θ : = 1 - 1 / p$ . By [F2] and step 1.1, $T u \in W^{θ, p} (\partial Ω)$ with $∥ T u ∥_{W^{θ, p} (\partial Ω)} \leq C (R, n, p) (∣ c ∣ R + ∣ d ∣)$ ; at $p = 1$ the same computation gives only $T u \in L^{1} (\partial Ω)$ , and no space $W^{0, 1}$ is introduced. For the $L^{p}$ value, parametrise the sphere by $x = R ω$ ; by [F3] and the definition of the surface integral, $∥ T u ∥_{L^{p} (\partial Ω)}^{p} = \int_{\partial Ω} ∣ c \cdot x + d ∣^{p} d S = R^{n - 1} \int_{S^{n - 1}} ∣ c \cdot R ω + d ∣^{p} d σ (ω)$ , which is the classical sphere integral.

3.1step 1.1step 2.1algebragiven∎

Conclusion. Steps 1.1 and 2.1 prove that the affine class lies in $W^{1, p} (Ω)$ with trace its classical restriction, that the trace lies in the fractional boundary space for $1 < p < \infty$ with the stated bound, and that its boundary $L^{p}$ norm is the displayed surface integral.

Source notes

Teschl's Theorem 9.18 (printed p. 209) is the statement $T f = f ∣_{\partial U}$ for continuous functions; Laugesen's Theorem 3.14 (printed pp. 62-64) records the classical boundary values, and Gagliardo's Teorema [1.I] (printed p. 289) the inverse estimate behind the fractional bound. The example keeps the endpoint $p = 1$ out of the fractional notation, as required by the page conventions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (archived 2025 author manuscript) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, complete 158-page graduate notes) (standard reference, not scraped)
Emilio Gagliardo, Caratterizzazioni delle tracce sulla frontiera relative ad alcune classi di funzioni in $n$ variabili, Rend. Sem. Mat. Univ. Padova 27 (1957), 284-305 (standard reference, not scraped)