TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Integer-order W^{k,2} and H^k agree with equivalent norms

Statement

Assume Countable Choice, let $n \geq 1$ and $k \in N_{0}$ , and use complex scalars. Write $W^{k, 2} = W^{k, 2} (R^{n}; C)$ for the weak-derivative Sobolev space of Integer-order Sobolev spaces and their norms, whose classes carry the weak derivatives $D^{α} f \in L^{2} (R^{n}; C)$ for $∣ α ∣ \leq k$ and the norm $∥ f ∥_{W^{k, 2}} = (\sum_{∣ α ∣ \leq k} ∥ D^{α} f ∥_{2}^{2})^{1 / 2},$ and let $H^{k} = H^{k} (R^{n})$ be the real-order Bessel-potential completion of Real-order Bessel-potential completion H^s with its canonical embedding $E_{k} : H^{k} \to S^{'} (R^{n})$ (The Bessel completion embeds canonically in tempered distributions). Let $u_{f} \in S^{'} (R^{n})$ denote the regular tempered distribution of an $L^{2}$ class $f$ . Then:

$E_{k} [H^{k}] = {u_{f} : f \in W^{k, 2}}$ , and $Φ (f) : = E_{k}^{- 1} (u_{f})$ is a bijection $Φ : W^{k, 2} \to H^{k}$ . Thus, under the regular-distribution embedding, $W^{k, 2}$ and $H^{k}$ are the same subspace of $S^{'} (R^{n})$ .
There are constants $0 < c_{k} \leq C_{k} < \infty$ , depending only on $n$ and $k$ , with $c_{k}^{1 / 2} ∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2} \leq ∥ f ∥_{W^{k, 2}} \leq C_{k}^{1 / 2} ∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2},$ and $∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2} = ∥ Φ (f) ∥_{H^{k}}$ . Hence the weak-derivative norm and the bracket-weighted $L^{2}$ norm are equivalent, and the latter is also equivalent to $∥ (1 + 4 π^{2} ∣ ξ ∣^{2})^{k / 2} F_{2} f ∥_{2}$ , by $∥ ⟨ ξ ⟩^{k} h ∥_{2} \leq ∥ (1 + 4 π^{2} ∣ ξ ∣^{2})^{k / 2} h ∥_{2} \leq (2 π)^{k} ∥ ⟨ ξ ⟩^{k} h ∥_{2}, h \in L^{2} .$
The three norm expressions are not identical in general: the bracket-weighted norm differs from both the weak-derivative norm and the Laplacian-weighted norm, as the Gaussian computation in the proof shows.

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , $k \in N_{0}$ , an $L^{2}$ class $f$ , and the multi-index conventions of $C^{k}$ maps and multi-index derivative notation in Euclidean space for $α \in N_{0}^{n}$ .

[A1]

Countable Choice is the hypothesis carried by every cited Sobolev, Fourier and regular-distribution interface below (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

$W^{k, p} (Ω; K)$ consists of $L^{p}$ classes $u$ such that for every $∣ α ∣ \leq k$ there is an $L^{p}$ class $D^{α} u$ whose locally integrable representative satisfies $\int u D^{α} φ = (- 1)^{∣ α ∣} \int D^{α} u φ$ for all $φ \in C_{c}^{\infty} (Ω)$ ; $D^{0} u = u$ ; the norm is the displayed finite- $p$ sum, and for $p = 2$ , $k = 0$ one has $W^{0, 2} = L^{2}$ (Integer-order Sobolev spaces and their norms).

[F2]

The weak-derivative test identity is equivalent to $\partial^{α} T_{u} = T_{v}$ in the sense of distributions; it is unchanged by almost-everywhere changes of $u$ and $v$ (Weak derivative of a locally integrable function, Weak differentiation ignores null-set changes), and a weak derivative is unique as an almost-everywhere class (Uniqueness of a weak derivative as an almost-everywhere class). The displayed $W^{k, p}$ formula is a genuine norm on classes (The Sobolev norm descends to equivalence classes).

[F3]

The completion $H^{s}$ carries the norm $∥ U ∥_{H^{s}} = \lim_{j} ∥ ⟨ ξ ⟩^{s} {\hat{u}}_{j} ∥_{2}$ of Cauchy sequences, and $E_{s} U = F^{- 1} (u_{w_{- s} J_{s} U})$ is a linear injection (Real-order Bessel-potential completion H^s, The Bessel completion embeds canonically in tempered distributions).

[F4]

For $s \in R$ let $M_{s} = {u \in S^{'} : w_{s} F u = u_{g} for some g \in L^{2}}$ , where $w_{s} (ξ) = ⟨ ξ ⟩^{s}$ and $w_{s} F u$ is distribution multiplication. Then $E_{s} : H^{s} \to M_{s}$ is a bijection, $g$ is unique, and $∥ E_{s}^{- 1} (u) ∥_{H^{s}} = ∥ g ∥_{2}$ (Weighted tempered-distribution characterization of H^s).

[F5]

For $L^{2}$ classes $f, h$ with $u_{f} = u$ and $u_{h} = \partial^{α} u$ , the Plancherel transforms satisfy $F_{2} h = (2 π i ξ)^{α} F_{2} f$ almost everywhere (Distributional derivatives are polynomial Fourier multipliers).

[F6]

$F (\partial^{α} u) = (2 π i ξ)^{α} F u$ in $S^{'} (R^{n})$ (Fourier differentiation and multiplication identities on tempered distributions).

[F7]

Plancherel $F_{2}$ is a surjective complex-linear isometry of $L^{2} (R^{n}; C)$ extending the Schwartz transform, so $∥ F_{2} h ∥_{2} = ∥ h ∥_{2}$ (Plancherel theorem, Complex Lp classes and Euclidean test-function conventions).

[F8]

For $h \in L^{1}$ , $F u_{h} = u_{\hat{h}}$ with the integral Fourier transform, and for $h \in L^{2}$ , $F u_{h} = u_{F_{2} h}$ ; every $L^{2}$ class defines a regular tempered distribution, and the regular-distribution map is injective after almost-everywhere identification. Hence the integral and Plancherel transforms agree almost everywhere for $h \in L^{1} \cap L^{2}$ (Fourier transform agrees with l one and plancherel transforms, Polynomial growth functions define tempered distributions, Locally integrable functions embed in distributions).

[F9]

Multiplication of a tempered distribution by a smooth polynomially bounded symbol $a$ is $⟨ a u, φ ⟩ = ⟨ u, a φ ⟩$ ; with the regular distribution $⟨ u_{h}, φ ⟩ = \int h φ$ of a locally integrable $h$ (Regular distribution from a locally integrable function) the same display with $u = u_{h}$ gives $a u_{h} = u_{a h}$ (Smooth polynomially bounded multipliers on schwartz space).

[F10]

Fourier transformation is a topological automorphism of $S^{'} (R^{n})$ , in particular injective (Fourier transform is a topological automorphism of tempered distributions).

[F11]

For $n \geq 1$ and $t > 0$ , $F (e^{- π t ∣ x ∣^{2}}) (ξ) = t^{- n / 2} e^{- π ∣ ξ ∣^{2} / t}$ , and every polynomial multiple of a positive Gaussian is absolutely integrable (Euclidean Gaussian transform with the 2π normalization).

[F12]

For every integer $m \geq 1$ and $a > 0$ , $r^{m} e^{- a r} \to 0$ as $r \to + \infty$ (The exponential dominates every fixed nonnegative integer power at $+ \infty$ ).

Proof

technique · compare the derivative-sum weight with the bracket weight and transfer the weighted tempered-distribution characterization. Throughout, $P_k(\xi)=\sum_{|\alpha|\le k}(2\pi)^{2|\alpha|}|\xi^\alpha|^2$ and $w_k(\xi)=\langle\xi\rangle^k$

1.1F1F2F5F7

Let $f \in W^{k, 2}$ and $∣ α ∣ \leq k$ . By [F1] the class $D^{α} f$ lies in $L^{2}$ , and by [F2] the weak-derivative test identity for $(f, D^{α} f)$ is equivalent to $\partial^{α} u_{f} = u_{D^{α} f}$ ; applying [F5] to the pair $(f, D^{α} f)$ gives $F_{2} (D^{α} f) = (2 π i ξ)^{α} F_{2} f$ almost everywhere, and [F7] gives $∥ D^{α} f ∥_{2} = ∥ (2 π i ξ)^{α} F_{2} f ∥_{2} < \infty$ . At $k = 0$ this is $D^{0} f = f$ and the Plancherel identity.

1.2algebra

The polynomial comparison. For $∣ α ∣ \leq k$ one has $(2 π)^{2 ∣ α ∣} \leq (2 π)^{2 k}$ and $∣ ξ^{α} ∣^{2} \leq ⟨ ξ ⟩^{2 k}$ ; indeed $∣ ξ^{α} ∣^{2} = \prod_{j} ∣ ξ_{j} ∣^{2 α_{j}} \leq \max (1, ∣ ξ ∣)^{2 ∣ α ∣}$ , which is $1 \leq (1 + ∣ ξ ∣^{2})^{k}$ when $∣ ξ ∣ < 1$ and at most $∣ ξ ∣^{2 k} \leq (1 + ∣ ξ ∣^{2})^{k}$ when $∣ ξ ∣ \geq 1$ . For the lower bound, if $∣ ξ ∣ \leq 1$ the $α = 0$ term equals $1$ while $⟨ ξ ⟩^{2 k} \leq 2^{k}$ ; if $∣ ξ ∣ \geq 1$ , some coordinate satisfies $∣ ξ_{j} ∣ = \max_{l} ∣ ξ_{l} ∣ \geq n^{- 1 / 2} ∣ ξ ∣$ , so the term $α = k e_{j}$ gives $P_{k} (ξ) \geq (2 π)^{2 k} ∣ ξ_{j} ∣^{2 k} \geq \frac{(2 π)^{2 k}}{n^{k}} ∣ ξ ∣^{2 k} \geq \frac{(2 π)^{2 k}}{(2 n)^{k}} ⟨ ξ ⟩^{2 k}$ , because $⟨ ξ ⟩^{2 k} = (1 + ∣ ξ ∣^{2})^{k} \leq 2^{k} ∣ ξ ∣^{2 k}$ . Hence $c_{k} ⟨ ξ ⟩^{2 k} \leq P_{k} (ξ) \leq C_{k} ⟨ ξ ⟩^{2 k}$ with $N_{k} : = # {α \in N_{0}^{n} : ∣ α ∣ \leq k}$ , $c_{k} : = \min (2^{- k}, \frac{(2 π)^{2 k}}{(2 n)^{k}}) > 0$ and $C_{k} : = N_{k} (2 π)^{2 k}$ ; at $k = 0$ both bounds equal $1$ .

1.3F2F4F6F8F9F10

Conversely, let $u \in M_{k}$ and let $g \in L^{2}$ satisfy $w_{k} F u = u_{g}$ as in [F4], so $g$ exists and is unique. Put $\hat{f} : = w_{k}^{- 1} g \in L^{2}$ and $f : = F_{2}^{- 1} \hat{f} \in L^{2}$ . First, $w_{k}^{- 1} (w_{k} F u) = F u$ and $w_{k}^{- 1} u_{g} = u_{\hat{f}}$ by applying [F9] to the smooth polynomially bounded symbols $w_{k}^{\pm 1}$ , so $F u = u_{\hat{f}} = u_{F_{2} f} = F (u_{f})$ by [F8], and injectivity of $F$ [F10] gives $u = u_{f}$ . Second, for each $∣ α ∣ \leq k$ put $v_{α} : = F_{2}^{- 1} ((2 π i ξ)^{α} \hat{f}) \in L^{2}$ , well defined since $∣ (2 π i ξ)^{α} \hat{f} ∣ \leq (2 π)^{k} ∣ g ∣$ by $∣ ξ^{α} ∣ \leq ⟨ ξ ⟩^{∣ α ∣}$ . Then $F (u_{v_{α}}) = u_{(2 π i ξ)^{α} \hat{f}}$ by [F8], while $F (\partial^{α} u_{f}) = (2 π i ξ)^{α} F u_{f} = u_{(2 π i ξ)^{α} \hat{f}}$ by [F6], [F8] and [F9]; injectivity [F10] gives $\partial^{α} u_{f} = u_{v_{α}}$ , so by [F2] the class $v_{α}$ is a weak $α$ -derivative of $f$ and equals $D^{α} f$ by uniqueness. Thus $f \in W^{k, 2}$ with $D^{α} f = v_{α}$ and $u = u_{f}$ .

1.4F7algebra

The second norm equivalence. For $h \in L^{2}$ and $k \geq 0$ the elementary estimates $1 + ∣ ξ ∣^{2} \leq 1 + 4 π^{2} ∣ ξ ∣^{2} \leq 4 π^{2} (1 + ∣ ξ ∣^{2})$ raise to the $k$ -th power to give $⟨ ξ ⟩^{2 k} \leq (1 + 4 π^{2} ∣ ξ ∣^{2})^{k} \leq (2 π)^{2 k} ⟨ ξ ⟩^{2 k}$ ; multiplying by $∣ h ∣^{2}$ and integrating yields $∥ ⟨ ξ ⟩^{k} h ∥_{2} \leq ∥ (1 + 4 π^{2} ∣ ξ ∣^{2})^{k / 2} h ∥_{2} \leq (2 π)^{k} ∥ ⟨ ξ ⟩^{k} h ∥_{2}$ . Applied to $h = F_{2} f$ this makes the bracket-weighted and Laplacian-weighted norms of the statement equivalent.

1.5F2F5F7F8F11F12algebra

Non-identity of the norms. Take $n = 1$ , $k = 1$ and $f (x) = e^{- π x^{2}}$ . By [F11] at $t = 1$ , $f \in L^{1}$ , while [F11] at $t = 2$ makes $f^{2}$ and $x^{2} f^{2}$ integrable, so $f, x f \in L^{2}$ . Its ordinary derivative $f^{'} = - 2 π x f$ is therefore in $L^{2}$ ; integration by parts against each compactly supported smooth test and [F2] show that $f \in W^{1, 2}$ with weak derivative $D f = f^{'}$ . The integral Fourier transform of $f$ equals $f$ by [F11], and the $L^{1}$ and $L^{2}$ distributional transform identities of [F8], followed by regular-distribution injectivity, give $F_{2} f = f$ almost everywhere. At frequency zero, [F11] with $t = 2$ gives $m : = ∥ f ∥_{2}^{2} = \int_{R} e^{- 2 π x^{2}} d x = 1 / \sqrt{2}$ . Integrating $(x e^{- 2 π x^{2}})^{'} = e^{- 2 π x^{2}} - 4 π x^{2} e^{- 2 π x^{2}}$ over $[- R, R]$ and letting $R \to \infty$ gives $\int_{R} x^{2} e^{- 2 π x^{2}} d x = m / (4 π)$ : the boundary term $2 R e^{- 2 π R^{2}}$ tends to zero by [F12], and both integrals converge by [F11]. Thus $∥ f^{'} ∥_{2}^{2} = 4 π^{2} \cdot m / (4 π) = π m$ , while [F5], [F7] give $∥ ∣ ξ ∣ \hat{f} ∥_{2}^{2} = ∥ f^{'} ∥_{2}^{2} / (4 π^{2}) = m / (4 π)$ . Hence $∥ f ∥_{W^{1, 2}}^{2} = m + π m = (1 + π) m$ , $∥ ⟨ ξ ⟩ \hat{f} ∥_{2}^{2} = m + m / (4 π) = (1 + 1 / (4 π)) m$ and $∥ (1 + 4 π^{2} ξ^{2})^{1 / 2} \hat{f} ∥_{2}^{2} = m + 4 π^{2} m / (4 π) = (1 + π) m$ ; the bracket value differs from both the weak-derivative value and the Laplacian-weighted value.

2.1F1F7step 1.1step 1.2

Let $f \in W^{k, 2}$ . Steps 1.1 and 1.2 give $∥ f ∥_{W^{k, 2}}^{2} = \sum_{∣ α ∣ \leq k} \int_{R^{n}} (2 π)^{2 ∣ α ∣} ∣ ξ^{α} ∣^{2} ∣ F_{2} f (ξ) ∣^{2} d ξ = \int_{R^{n}} P_{k} (ξ) ∣ F_{2} f (ξ) ∣^{2} d ξ$ , a finite sum of finite integrals, and therefore $c_{k} ∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2}^{2} \leq ∥ f ∥_{W^{k, 2}}^{2} \leq C_{k} ∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2}^{2}$ ; in particular $⟨ ξ ⟩^{k} F_{2} f \in L^{2}$ with $∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2} \leq c_{k}^{- 1 / 2} ∥ f ∥_{W^{k, 2}}$ .

3.1F3F4F8F9step 2.1

Let $f \in W^{k, 2}$ . Step 2.1 makes $w_{k} F_{2} f \in L^{2}$ , so [F8] gives $F (u_{f}) = u_{F_{2} f}$ and [F9] gives $w_{k} F (u_{f}) = u_{w_{k} F_{2} f}$ ; hence $u_{f} \in M_{k}$ in the notation of [F4]. Therefore $U : = Φ (f) = E_{k}^{- 1} (u_{f}) \in H^{k}$ is defined, using the injection $E_{k}$ of [F3], and [F4] with $g = w_{k} F_{2} f$ gives $∥ U ∥_{H^{k}} = ∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2}$ .

4.1F3F4F8step 1.3step 3.1

The identification. Step 3.1 shows ${u_{f} : f \in W^{k, 2}} \subseteq M_{k}$ and step 1.3 shows $M_{k} \subseteq {u_{f} : f \in W^{k, 2}}$ ; since [F4] gives $M_{k} = E_{k} [H^{k}]$ , the two sets are equal. The map $Φ (f) = E_{k}^{- 1} (u_{f})$ is defined on all of $W^{k, 2}$ and injective, because $u_{f} = u_{h}$ forces $f = h$ almost everywhere by the regular-distribution injection [F8]; it is surjective, because every $U \in H^{k}$ has $E_{k} U \in M_{k} = u_{f}$ for some $f \in W^{k, 2}$ by step 1.3, so $Φ (f) = U$ . Hence $Φ$ is a bijection and $E_{k} [H^{k}] = {u_{f} : f \in W^{k, 2}}$ .

4.2F7step 2.1step 3.1

The first norm equivalence. For $f \in W^{k, 2}$ , step 2.1 gives $∥ f ∥_{W^{k, 2}} \leq C_{k}^{1 / 2} ∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2}$ and $c_{k}^{1 / 2} ∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2} \leq ∥ f ∥_{W^{k, 2}}$ , while step 3.1 identifies $∥ ⟨ ξ ⟩^{k} F_{2} f ∥_{2} = ∥ Φ (f) ∥_{H^{k}}$ ; at $k = 0$ , $c_{0} = C_{0} = 1$ and this is the Plancherel identity.

5.1A1step 1.4step 1.5step 4.1step 4.2∎

Steps 4.1 (bijection and equality of subspaces), 4.2 (weak-derivative and bracket norms equivalent with constants $c_{k}^{1 / 2}, C_{k}^{1 / 2}$ ), 1.4 (bracket and Laplacian-weighted norms equivalent with constants $1, (2 π)^{k}$ ) and 1.5 (not identical in general) prove statements 1-3, including the cases $k = 0$ and $n = 1$ handled above; Countable Choice is used only through the cited interfaces.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

102 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

Semyon Dyatlov, Lecture Notes for 18.155, current revision (standard reference, not scraped)
Richard B. Melrose, Differential Analysis, Chapter 3: Distributions (standard reference, not scraped)