LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 partial-trace displacement space is a Hilbert space

Statement

Assume the geometry and trace conventions of Partial-trace displacement space on a polygon. Then the maps $T_{D}, T_{C} : H^{1} (Ω; R^{2}) \to L^{2} (Γ_{D}; R^{2}), L^{2} (Γ_{C}; R^{2})$ are bounded and linear, and $V = \ker T_{D}$ is a Hilbert space with the inherited $H^{1}$ inner product.

Facts & Assumptions

Given: The bounded connected polygon, its fixed bounded $C^{1}$ collars $U_{D}, U_{C}$ , and the trace maps defined in Partial-trace displacement space on a polygon.

[A1]

The Axiom of Choice is assumed by the bounded C1 trace theorem and its smooth-density interface. (The Axiom of Choice, The $L^{p}$ trace operator on a bounded $C^{1}$ domain)

[F1]

On a bounded $C^{1}$ domain $U$ , $T_{U} : H^{1} (U; R^{2}) \to L^{2} (\partial U; R^{2})$ is bounded and linear, agrees with boundary restriction for Sobolev functions having a representative continuous on $\overline{U}$ , and satisfies $∥ T_{U} w ∥_{L^{2} (\partial U)} \leq C_{U} ∥ w ∥_{H^{1} (U)}$ . (The $L^{p}$ trace operator on a bounded $C^{1}$ domain)

[F2]

Restriction from $H^{1} (Ω)$ to $H^{1} (U_{j})$ is well defined and does not increase the $H^{1}$ norm when $U_{j} \subset Ω$ . (Sobolev extension domains and extension operators, Integer-order Sobolev spaces and their norms)

[F3]

$H^{1} (Ω; R^{2})$ is complete, and a closed subspace of a complete inner-product space is complete. (Integer-order Sobolev spaces are Banach, Closed subspaces of complete metric spaces are complete; the converse under countable choice)

Proof

technique · direct

Given: The fixed collars and the trace maps $T_{D}, T_{C}$ on the bounded connected polygon $Ω$ .

1.1A1F1F2given

For $j \in {D, C}$ , restriction [F2] followed by the bounded trace map [F1] and restriction from $\partial U_{j}$ to its segment $Γ_{j}$ gives $∥ T_{j} v ∥_{L^{2} (Γ_{j})} \leq C_{j} ∥ v ∣_{U_{j}} ∥_{H^{1} (U_{j})} \leq C_{j} ∥ v ∥_{H^{1} (Ω)}$ for every $v \in H^{1} (Ω; R^{2})$ . Both maps are compositions of linear maps, so they are bounded and linear.

2.1F1F3step 1.1∎

The space $V$ is the kernel of the bounded linear map $T_{D}$ , hence is closed in $H^{1} (Ω; R^{2})$ ; by [F3] the inherited inner product is complete on $V$ , so $V$ is Hilbert.

Depends on

Used by

Cited to discharge well-definedness by Partial-trace displacement space on a polygon.

Dependency tree · two levels

43 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

Jean-Luc Guermond, MATH 661 Fall 2025, Part XI Chapter 53: Stokes equations: Basic ideas (standard reference, not scraped)
Walter Zulehner, Numerical Methods for Continuum Mechanics 1, complete 80-page lecture notes (standard reference, not scraped)