LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 zero-boundary Sobolev evolution triple on an arbitrary bounded open set

Statement

Assume Countable Choice. Let $U \subset R^{d}$ be bounded and open, $d \geq 1$ , and put $H = L^{2} (U; R)$ and $V = H_{0}^{1} (U; R)$ , where the latter is the $H^{1}$ -closure of $C_{c}^{\infty} (U)$ . Then $V$ is a separable real Hilbert space, its inclusion into $H$ is continuous, injective and dense, and $(V, H, V^{*})$ is a real evolution triple. The gradient norm and the full $H^{1}$ norm are equivalent on $V$ . No regularity of $\partial U$ is required.

Statement references

Clason, Chapter 11: the Sobolev evolution-triple setting

Facts & Assumptions

Given: Countable Choice, a bounded open $U \subset R^{d}$ , and the stated real spaces.

[A1]

Countable Choice is carried by the $L^{2}$ completeness and density suppliers and by the countable selections below (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

$L^{2} (U)$ is a real Hilbert space; rational box-step functions are countable and dense in $L^{2} (R^{d})$ ( $L^{2}$ with the integral pairing is a Hilbert space, Rational box-step functions form a countable dense subset of $L^{p} (R^{n})$ for $1 \leq p < \infty$ ).

[F2]

Weak derivatives are defined by integration against compactly supported smooth tests; $H_{0}^{1} (U)$ is the $H^{1}$ -closure of those smooth functions (Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure).

[F3]

On an open set bounded in one direction, $∥ v ∥_{2} \leq C ∥ D v ∥_{2}$ for $v \in H_{0}^{1} (U)$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction).

[F4]

$C_{c}^{\infty} (U)$ is dense in $L^{2} (U)$ for every open $U$ (Smooth compactly supported functions of an open set are dense in $L^{2}$ ).

[F5]

A continuous dense injective Hilbert inclusion $V ↪ H$ defines the canonical real evolution triple (Evolution triples and the parabolic energy space).

Proof

1.1givenA1F1construct

If $U = \emptyset$ , both spaces are zero and the conclusions hold. Otherwise choose finite $a < b$ with $U \subset {a < x_{1} < b}$ . The zero extension of any $h \in H$ belongs to $L^{2} (R^{d})$ with the same norm. Restricting the countable dense box-step family in [F1] to $U$ therefore gives a countable dense subset of $H$ . The product $Z = H^{d + 1}$ is a separable Hilbert space.

2.1F1F2step 1.1algebra

The map $J : H^{1} (U) \to Z$ , $J (v) = (v, D_{1} v, \dots, D_{d} v)$ , is an isometry for the full Sobolev norm. Its range is closed: if $J (v_{n}) \to (v, g_{1}, \dots, g_{d})$ in $Z$ , then for every $ϕ \in C_{c}^{\infty} (U)$ , Cauchy–Schwarz gives $\int v D_{i} ϕ = \lim_{n} \int v_{n} D_{i} ϕ = - \lim_{n} \int D_{i} v_{n} ϕ = - \int g_{i} ϕ$ . Thus $g_{i} = D_{i} v$ weakly, so the limit is $J (v)$ . A closed subspace of a Hilbert space is complete, hence $H^{1} (U)$ is Hilbert.

3.1F2F3step 1.1step 2.1algebra

By the closure definition, $V$ is a closed subspace of $H^{1} (U)$ and is Hilbert. The Poincare inequality applies because $U$ is bounded in the first direction, and yields $∥ D v ∥_{2}^{2} \leq ∥ v ∥_{H^{1}}^{2} \leq (1 + C^{2}) ∥ D v ∥_{2}^{2}$ on $V$ . This proves norm equivalence and continuity of the inclusion $V ↪ H$ . Injectivity holds because these spaces use the same almost-everywhere equivalence classes.

4.1A1step 1.1step 2.1step 3.1construct

A subspace $Y$ of a separable metric space $Z$ is separable under [A1]: if $(z_{j})$ is dense in $Z$ , the sets $Y \cap B (z_{j}, r)$ for positive rational $r$ form a countable base of $Y$ ; choose one point from every nonempty such set. Any relatively open neighborhood contains one of these sets, so the chosen points are dense. Apply this first to $J (H^{1} (U)) \subset Z$ and then to $J (V)$ ; transport the dense subsets through the isometry $J$ . Thus $V$ is separable.

5.1F2F4F5step 3.1step 4.1algebra∎

By [F4], $C_{c}^{\infty} (U)$ is dense in $H$ , and it is contained in $V$ by [F2]. Thus $V ↪ H$ is dense. The Hilbert, separability, continuity and injectivity conclusions already proved give the canonical evolution triple by [F5]. Every argument used an arbitrary bounded open $U$ , so none requires a boundary chart or a polyhedral boundary.

Source notes

This reproduces the actual argument of the read published polyhedral Sobolev-evolution supplier on the larger bounded-open-set domain class. Its closed-graph, separability and compact-smooth-density arguments do not use polyhedral geometry. The bibliographic reference records the evolution-space context; no new reading of Clason's full text is claimed here.

Depends on

Used by

Dependency tree · two levels

63 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

Christian Clason, Introduction to Finite Element Methods (standard reference, not scraped)