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 absolute value preserves the L^2 norm and the Dirichlet energy on H^1_0

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $n \geq 1$ , let $Ω \subseteq R^{n}$ be open, and let $u \in H_{0}^{1} (Ω; R)$ (Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms). Then $∣ u ∣ \in H_{0}^{1} (Ω)$ , $∥ ∣ u ∣ ∥_{L^{2} (Ω)} = ∥ u ∥_{L^{2} (Ω)}$ (The space $L^{p} (μ)$ as the quotient by null functions), and $\int_{Ω} ∣ D ∣ u ∣ ∣^{2} d x = \int_{Ω} ∣ D u ∣^{2} d x .$ Consequently the constrained minimisation of the Dirichlet energy on the $L^{2}$ -unit sphere may be restricted to nonnegative competitors.

Facts & Assumptions

Given: An open set $Ω \subseteq R^{n}$ , $n \geq 1$ , and a real class $u \in H_{0}^{1} (Ω)$ .

[A1]

The Axiom of Choice: the Axiom of Choice, inherited through the Sobolev composition and subsequence suppliers.

[A2]

AC implies DC implies countable choice: the Axiom of Choice implies Countable Choice, so [F4] applies under the Statement's assumption.

[F1]

Positive, negative, and truncated Sobolev functions: for a real Sobolev class $v$ , $∣ v ∣ \in H^{1} (Ω)$ and $D ∣ v ∣ = sgn (v) D v$ a.e., with $D v = 0$ a.e. on ${v = 0}$ ; also $∣ v ∣ = v^{+} + v^{-}$ .

[F2]

Integer-order Sobolev spaces and their norms: $H^{1} (Ω)$ is the space of $L^{2}$ classes with all first weak derivatives in $L^{2}$ , with norm controlling both $∥ v ∥_{L^{2}}$ and $∥ D v ∥_{L^{2}}$ .

[F3]

Zero-boundary Sobolev space as a norm closure: $H_{0}^{1} (Ω)$ is the closure of $C_{c}^{\infty} (Ω)$ in $H^{1} (Ω)$ and is closed in that norm.

[F4]

Assuming Countable Choice, $L^{p}$ -convergent sequences have almost-everywhere convergent subsequences: if a sequence converges in $L^{2} (Ω)$ , it has a subsequence converging almost everywhere.

[F5]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : for smooth $v$ and a smooth scalar function $Φ$ , $D (Φ \circ v) = Φ^{'} (v) D v$ .

[F6]

Dominated convergence: an almost-everywhere convergent sequence dominated by an integrable function has convergent integrals.

[F7]

The space $L^{p} (μ)$ as the quotient by null functions: $L^{2}$ norms and pointwise compositions are well defined on almost-everywhere classes.

Proof

technique · direct

Given: The open set $Ω$ and real class $u \in H_{0}^{1} (Ω)$ above.

1.1F1F3F5F6

(Smooth compactly supported case). Fix $v \in C_{c}^{\infty} (Ω; R)$ and, for $ε > 0$ , set $Φ_{ε} (s) = \sqrt{s^{2} + ε^{2}} - ε$ . Then $Φ_{ε}$ is smooth, $Φ_{ε} (0) = 0$ , $0 \leq Φ_{ε} (s) \leq ∣ s ∣$ , and $∣ Φ_{ε}^{'} (s) ∣ \leq 1$ . Thus $Φ_{ε} \circ v \in C_{c}^{\infty} (Ω)$ . As $ε ↓ 0$ , the squared value error is bounded by $∣ v ∣^{2} \in L^{1}$ and tends pointwise to zero, so $Φ_{ε} (v) \to ∣ v ∣$ in $L^{2}$ by [F6]. By [F5], $D (Φ_{ε} (v)) = Φ_{ε}^{'} (v) D v$ ; the squared gradient error tends pointwise to zero and is bounded by $4 ∣ D v ∣^{2} \in L^{1}$ , so [F1] and [F6] give convergence to $D ∣ v ∣$ in $L^{2}$ . Hence $Φ_{ε} (v) \to ∣ v ∣$ in $H^{1}$ , so $∣ v ∣ \in H_{0}^{1} (Ω)$ by [F3].

2.1A2F2F3F4

(Approximation and almost-everywhere convergence). By [F3] choose $v_{j} \in C_{c}^{\infty} (Ω)$ with $v_{j} \to u$ in $H^{1}$ . In particular $v_{j} \to u$ in $L^{2}$ ; by [A2], Countable Choice is available, so [F4] lets us pass to a subsequence, still denoted $v_{j}$ , with $v_{j} \to u$ almost everywhere. Step 1.1 gives $∣ v_{j} ∣ \in H_{0}^{1} (Ω)$ for every $j$ . The pointwise inequality $∣ ∣ v_{j} ∣ - ∣ u ∣ ∣ \leq ∣ v_{j} - u ∣$ shows $∣ v_{j} ∣ \to ∣ u ∣$ in $L^{2}$ .

3.1step 2.1F1F6

(Convergence of the gradients). By [F1], $D ∣ v_{j} ∣ - D ∣ u ∣ = sgn (v_{j}) (D v_{j} - D u) + (sgn (v_{j}) - sgn (u)) D u .$ The first term tends to zero in $L^{2}$ because $∣ sgn (v_{j}) ∣ \leq 1$ and $D v_{j} \to D u$ in $L^{2}$ . For the second, at almost every point where $u \neq 0$ the signs converge by the pointwise convergence in step 2.1; on ${u = 0}$ one has $D u = 0$ a.e. by [F1]. Thus its squared magnitude tends to zero a.e. and is bounded by $4 ∣ D u ∣^{2} \in L^{1}$ , so [F6] gives convergence to zero in $L^{2}$ . Therefore $D ∣ v_{j} ∣ \to D ∣ u ∣$ in $L^{2}$ .

4.1step 2.1step 3.1F1F3F7A1A2∎

Since $∣ v_{j} ∣ \to ∣ u ∣$ in $H^{1}$ by steps 2.1-3.1 and $H_{0}^{1} (Ω)$ is closed by [F3], $∣ u ∣ \in H_{0}^{1} (Ω)$ . Pointwise $∣ ∣ u ∣ ∣ = ∣ u ∣$ , so the $L^{2}$ norms agree by [F7]; and [F1], including $D u = 0$ a.e. on ${u = 0}$ , gives $∣ D ∣ u ∣ ∣ = ∣ D u ∣$ a.e., hence equality of the Dirichlet energies. Consequently every unit-sphere competitor $u$ is replaced by the nonnegative competitor $∣ u ∣$ with the same energy, so the infimum is unchanged when minimisation is restricted to nonnegative competitors. The Axiom of Choice enters only through the declared composition and subsequence suppliers.

Depends on

Used by

The first Dirichlet eigenfunction by constrained minimisation Theorem

Dependency tree · two levels

56 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

Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (2011) (standard reference, not scraped)