LemmaStatement: AI-adaptedProof: 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 gradient norm dominates the H-one norm on zero-boundary Sobolev space

Statement

Assume the Axiom of Choice (The Axiom of Choice), used to invoke the published Sobolev completeness theorem through its Countable-Choice interface (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $Ω \subseteq (- L, L)^{3}$ be bounded and open for some $L > 0$ , and write $H^{1} (Ω) = W^{1, 2} (Ω; R)$ with the norm of Integer-order Sobolev spaces and their norms, and $H_{0}^{1} (Ω) : = W_{0}^{1, 2} (Ω; R)$ , the closure of $C_{c}^{\infty} (Ω; R)$ in that norm (Zero-boundary Sobolev space as a norm closure). Then $H^{1} (Ω)$ is complete, $H_{0}^{1} (Ω)$ is a closed subspace and is complete, the $W^{1, 2}$ quadratic norm is a Hilbert norm (its coordinate $L^{2}$ pairings satisfy the parallelogram law), and

$∥ v ∥_{L^{2}}^{2} \leq (2 L)^{2} ∥ \partial_{1} v ∥_{L^{2}}^{2} \leq (2 L)^{2} ∥ \nabla v ∥_{L^{2}}^{2} for every v \in H_{0}^{1} (Ω) .$

In particular $∥ v ∥_{L^{2}} \leq 2 L ∥ \nabla v ∥_{L^{2}}$ and the gradient norm is equivalent to the full $H^{1}$ norm on $H_{0}^{1} (Ω)$ . The argument needs neither a smooth domain nor a general boundary-trace theorem, and no choice beyond the completeness interface is used.

Facts & Assumptions

Given: The Axiom of Choice $A C$ (so Countable Choice ${A C}_{ω}$ holds), a number $L > 0$ , and a bounded open $Ω \subseteq (- L, L)^{3}$ . Write $H^{1} = W^{1, 2} (Ω; R)$ and $H_{0}^{1} = W_{0}^{1, 2} (Ω; R)$ , with $∥ u ∥_{W}^{2} = ∥ u ∥_{2}^{2} + ∥ \nabla u ∥_{2}^{2} = ∥ u ∥_{2}^{2} + \sum_{j = 1}^{3} ∥ \partial_{j} u ∥_{2}^{2}$ .

[A1]

The Axiom of Choice implies the Axiom of Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Sobolev spaces and norm. For open $Ω \subseteq R^{n}$ , $W^{k, p} (Ω; K)$ consists of the $L^{p}$ classes whose weak derivatives up to order $k$ are $L^{p}$ classes, the $D^{α} u$ are well-defined classes and $∥ u ∥_{W^{k, p}} = (\sum_{∣ α ∣ \leq k} ∥ D^{α} u ∥_{L^{p}}^{p})^{1 / p}$ for $p < \infty$ ; at $k = 1$ , $p = 2$ this is $∥ u ∥_{W}^{2} = ∥ u ∥_{2}^{2} + ∥ \nabla u ∥_{2}^{2}$ (Integer-order Sobolev spaces and their norms). The definition leaves the norm axioms separate; under AC they are supplied by the complete-normed-space assertion of [F3].

[F2]

Zero-boundary space as a closure. $W_{0}^{k, p} (Ω; K)$ is the metric closure of $C_{c}^{\infty} (Ω; K)$ in $W^{k, p}$ , so $u \in W_{0}^{k, p}$ exactly when for every $δ > 0$ there is $φ \in C_{c}^{\infty} (Ω; K)$ with $∥ u - φ ∥_{W^{k, p}} < δ$ ; no boundary trace is asserted (Zero-boundary Sobolev space as a norm closure).

[F3]

Completeness. Under the Axiom of Choice, $W^{k, p} (Ω; K)$ with the displayed norm is a complete normed space; at $k = 1$ , $p = 2$ , $H^{1}$ is complete (Integer-order Sobolev spaces are Banach).

[F4]

Hilbert structure of real $L^{2}$ . Under ${A C}_{ω}$ , real $L^{2} (Ω)$ with $⟨ f, g ⟩ = \int f g$ is a real Hilbert space and $⟨ f, f ⟩ = ∥ f ∥_{2}^{2}$ ( $L^{2}$ with the integral pairing is a Hilbert space); in every real inner-product space the parallelogram law $∥ x + y ∥^{2} + ∥ x - y ∥^{2} = 2 ∥ x ∥^{2} + 2 ∥ y ∥^{2}$ holds (The parallelogram law).

[F5]

Cauchy-Schwarz for $L^{2}$ . $\int ∣ f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ for $f, g \in L^{2}$ (Cauchy-Schwarz inequality for $L^{2}$ ); applied to $g = 1_{(- L, L)}$ this gives $(\int_{- L}^{L} ∣ f ∣)^{2} \leq 2 L \int_{- L}^{L} ∣ f ∣^{2}$ .

[F6]

Newton-Leibniz with interior derivative. If $G : [a, b] \to R$ is continuous on $[a, b]$ , differentiable on $(a, b)$ , and $f$ is Riemann integrable with $f = G^{'}$ on $(a, b)$ , then $\int_{a}^{b} f = G (b) - G (a)$ (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[F7]

Tonelli. A nonnegative measurable function on a $σ$ -finite product may be integrated in either order (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F8]

Norm axioms. A norm satisfies $∥ x + y ∥ \leq ∥ x ∥ + ∥ y ∥$ and $∥ x ∥ = 0 \Rightarrow x = 0$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms), so a limit of a sequence in a subspace that exists in an ambient complete space and is approached by elements of the subspace lies in its closure whenever the closure is closed for the norm topology.

Proof

technique · direct

1.1givenA1F1F3

By [F3] the space $H^{1}$ is complete for $∥ u ∥_{W}^{2} = ∥ u ∥_{2}^{2} + ∥ \nabla u ∥_{2}^{2}$ ; the Axiom of Choice assumed here is used only to supply Countable Choice for that theorem by [A1].

1.2givenF6

Let $v \in C_{c}^{\infty} (Ω; R)$ and extend it by zero to $R^{3}$ ; fix $(x_{2}, x_{3}) \in R^{2}$ and let $G (s) = v (s, x_{2}, x_{3})$ . Since $Ω \subseteq (- L, L)^{3}$ and $v$ vanishes outside $Ω$ , $G$ is continuous on $[- L, L]$ , differentiable on $(- L, L)$ with $G^{'} = \partial_{1} v (\cdot, x_{2}, x_{3})$ Riemann integrable, and $G (- L) = 0$ ; hence [F6] gives $v (x_{1}, x_{2}, x_{3}) = \int_{- L}^{x_{1}} \partial_{1} v (s, x_{2}, x_{3}) d s$ for every $x_{1} \in (- L, L)$ .

2.1step 1.1F1F2F3F8algebra

$H_{0}^{1}$ is a closed subspace of $H^{1}$ and is complete: if $(u_{m}) \subseteq H_{0}^{1}$ is $∥ \cdot ∥_{W}$ -Cauchy, [F3] gives $u \in H^{1}$ with $∥ u_{m} - u ∥_{W} \to 0$ ; given $δ > 0$ choose $m$ with $∥ u_{m} - u ∥_{W} < δ$ and then, because $u_{m} \in H_{0}^{1}$ , a test function $φ \in C_{c}^{\infty} (Ω; R)$ with $∥ u_{m} - φ ∥_{W} < δ$ by [F2]; the triangle inequality [F8] gives $∥ u - φ ∥_{W} < 2 δ$ , so $u \in H_{0}^{1}$ by the characterization [F2], and $∥ u_{m} - u ∥_{W} \to 0$ in the subspace norm; the identical argument with $H_{0}^{1}$ in place of the arbitrary subspace shows closedness of $H_{0}^{1}$ in $H^{1}$ .

2.2step 1.1F1F4algebra

The $W^{1, 2}$ norm is a Hilbert norm: writing $∥ u ∥_{W}^{2} = \sum_{∣ α ∣ \leq 1} ∥ D^{α} u ∥_{2}^{2}$ by [F1], each summand $∥ D^{α} u ∥_{2}^{2}$ is the squared norm of the real Hilbert space $L^{2} (Ω)$ by [F4], so the parallelogram law [F4] holds for each summand and, summed over the finite index set ${∣ α ∣ \leq 1}$ , for $∥ \cdot ∥_{W}^{2}$ itself; combining this with the completeness of step 1.1 exhibits $H^{1}$ and its closed subspace $H_{0}^{1}$ as real Hilbert spaces for the coordinate $L^{2}$ pairings.

2.3step 1.2F5algebra

For such $v$ and every $x = (x_{1}, x_{2}, x_{3})$ , step 1.2 and the Cauchy-Schwarz bound [F5] give $∣ v (x) ∣^{2} \leq (\int_{- L}^{L} ∣ \partial_{1} v (s, x_{2}, x_{3}) ∣ d s)^{2} \leq 2 L \int_{- L}^{L} ∣ \partial_{1} v (s, x_{2}, x_{3}) ∣^{2} d s$ .

3.1step 2.3F7algebra

Integrating the inequality of step 2.3 over $(- L, L)^{3}$ and applying Tonelli [F7] to the nonnegative integrand gives $∥ v ∥_{L^{2}}^{2} \leq 2 L \int_{(- L, L)^{3}} \int_{- L}^{L} ∣ \partial_{1} v (s, x_{2}, x_{3}) ∣^{2} d s d x = (2 L)^{2} ∥ \partial_{1} v ∥_{L^{2}}^{2}$ , because the $x_{1}$ -integration contributes the length $2 L$ and $v$ vanishes outside the box.

4.1step 3.1F1F2F8algebra

Fix $v \in H_{0}^{1}$ and $δ > 0$ . By [F2] choose one $φ \in C_{c}^{\infty} (Ω)$ with $∥ φ - v ∥_{W} < δ$ . The triangle inequality and step 3.1 give $∥ v ∥_{2} \leq δ + ∥ φ ∥_{2} \leq δ + 2 L ∥ \partial_{1} φ ∥_{2} \leq 2 L ∥ \partial_{1} v ∥_{2} + (1 + 2 L) δ$ . Since this holds for every $δ > 0$ , $∥ v ∥_{2} \leq 2 L ∥ \partial_{1} v ∥_{2}$ ; squaring and using $∥ \partial_{1} v ∥_{2} \leq ∥ \nabla v ∥_{2}$ gives the displayed chain. This uses one approximant for each fixed tolerance, without selecting an approximation sequence.

5.1step 2.1step 2.2step 4.1F1algebra∎

Equivalence of norms on $H_{0}^{1}$ : $∥ \nabla v ∥_{2} \leq ∥ v ∥_{W}$ is immediate from $∥ v ∥_{W}^{2} = ∥ v ∥_{2}^{2} + ∥ \nabla v ∥_{2}^{2}$ by [F1], while step 4.1 gives $∥ v ∥_{W}^{2} = ∥ v ∥_{2}^{2} + ∥ \nabla v ∥_{2}^{2} \leq (1 + (2 L)^{2}) ∥ \nabla v ∥_{2}^{2}$ ; the gradient norm is therefore equivalent to the full $W^{1, 2}$ norm on $H_{0}^{1}$ , both operators being applied to the weak derivatives of [F1] and no smoothness of $Ω$ being used. This proves all the claims of the Statement, and no choice beyond the completeness interface [F3]/[A1] has been used.

Depends on

Dependency tree · 2 levels

Sources

J. K. Hunter, Notes on Partial Differential Equations (University of California, Davis; revised 6/18/2014), Chapter 4.4 (Theorem 4.9, Eq. 4.11: the Poincare inequality for H_0^1)