TheoremStatement: 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.

Every $H^{- 1}$ functional is an $L^{2}$ function plus a divergence

Statement

Assume Countable Choice. Let $Ω \subseteq R^{n}$ be open, $n \geq 1$ . For every $F \in H^{- 1} (Ω)$ (The negative Sobolev space $H^{- 1} (Ω)$ ) there are $f_{0}, f_{1}, \dots, f_{n} \in L^{2} (Ω)$ such that $F (v) = (f_{0}, v)_{L^{2}} + \sum_{i = 1}^{n} (f_{i}, D_{i} v)_{L^{2}} for every v \in H_{0}^{1} (Ω),$ the norm is exactly the infimum over all such representations, $∥ F ∥_{H^{- 1}} = \inf {(\sum_{i = 0}^{n} ∥ f_{i} ∥_{L^{2}}^{2})^{1 / 2} : F (v) = (f_{0}, v)_{L^{2}} + \sum_{i = 1}^{n} (f_{i}, D_{i} v)_{L^{2}} \forall v},$ and the infimum is attained by the canonical choice $f_{0} = g$ , $f_{i} = D_{i} g$ given by the Riesz vector of $\overline{F (\cdot)}$ ; in particular the data are controlled by the norm and conversely. The representation is the converse of $L^{2}$ forcing and divergence data embed in $H^{- 1}$ with a quantitative bound and needs no Hahn--Banach extension theorem: Riesz representation in $H_{0}^{1}$ already produces it.

Facts & Assumptions

Given: Countable Choice; an open $Ω \subseteq R^{n}$ , $n \geq 1$ ; and a functional $F \in H^{- 1} (Ω)$ , that is, a bounded conjugate-linear functional on $H_{0}^{1} (Ω)$ with $∥ F ∥_{H^{- 1}} = \sup_{∥ v ∥ \leq 1} ∣ F (v) ∣$ .

[F1]

$H_{0}^{1} (Ω)$ is a Hilbert space under $(u, v)_{H^{1}} : = (u, v)_{L^{2}} + \sum_{i = 1}^{n} (D_{i} u, D_{i} v)_{L^{2}}$ , whose induced norm is the $W^{1, 2}$ norm; the pairing is linear in the first variable and conjugate-linear in the second, and conjugate-symmetric (The Sobolev space $H^{1}$ is a Hilbert space, Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure, The notation $H^{k}$ and the reserved zero-boundary symbol, Hilbert space).

[F2]

$H^{- 1} (Ω)$ consists of the bounded conjugate-linear functionals, with $∥ F ∥_{H^{- 1}} = \sup_{∥ v ∥ \leq 1} ∣ F (v) ∣$ ; the $L^{2}$ pairings are conjugate-symmetric and depend only on classes (The negative Sobolev space $H^{- 1} (Ω)$ , The space $L^{p} (μ)$ as the quotient by null functions).

[F3]

Riesz representation under Countable Choice: for a bounded linear functional $G$ on $H_{0}^{1} (Ω)$ there is a unique $g$ with $G (v) = (v, g)_{H^{1}}$ for all $v$ , and $∥ G ∥ = ∥ g ∥_{H^{1}}$ , the operator norm being the dual norm (Riesz representation for Hilbert spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F4]

Every $L^{2}$ pairing satisfies $∣ (f, v)_{L^{2}} ∣ \leq ∥ f ∥_{2} ∥ v ∥_{2}$ by $L^{2}$ with the integral pairing is a Hilbert space and Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs. Conjugation and finite Cauchy--Schwarz: $\overline{z}$ has $∣ \overline{z} ∣ = ∣ z ∣$ and $\overline{F (v)}$ depends linearly on $v$ when $F$ is conjugate-linear; for complex numbers $z_{0}, \dots, z_{n}, w_{0}, \dots, w_{n}$ , $∣ \sum_{i = 0}^{n} z_{i} \overline{w_{i}} ∣ \leq (\sum_{i = 0}^{n} ∣ z_{i} ∣^{2})^{1 / 2} (\sum_{i = 0}^{n} ∣ w_{i} ∣^{2})^{1 / 2}$ (Real and imaginary parts, complex conjugation, and modulus, Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

Proof

1.1F1F4

The functional $G (v) : = \overline{F (v)}$ is linear in $v$ (conjugating a conjugate-linear map gives a linear one), and $∣ G (v) ∣ = ∣ F (v) ∣$ for every $v$ , so $G$ is bounded with the same dual norm as $F$ .

1.2F1F2F4

Every representation bounds the norm: if $F (v) = (f_{0}, v)_{L^{2}} + \sum_{i} (f_{i}, D_{i} v)_{L^{2}}$ for all $v$ , then the $L^{2}$ pairing bound followed by finite Cauchy--Schwarz on the real vectors of component norms, and $∥ v ∥_{H^{1}}^{2} = ∥ v ∥_{L^{2}}^{2} + \sum_{i} ∥ D_{i} v ∥_{L^{2}}^{2}$ give $∣ F (v) ∣ \leq (\sum_{i = 0}^{n} ∥ f_{i} ∥_{L^{2}}^{2})^{1 / 2} ∥ v ∥_{H^{1}},$ so $∥ F ∥_{H^{- 1}} \leq (\sum_{i = 0}^{n} ∥ f_{i} ∥_{L^{2}}^{2})^{1 / 2}$ and, taking the infimum over all representations, $∥ F ∥_{H^{- 1}} \leq \inf {\dots}$ .

2.1F1F2F3F4step 1.1

Riesz representation: by [F3] applied to the Hilbert space $H_{0}^{1} (Ω)$ there is a unique $g \in H_{0}^{1} (Ω)$ with $G (v) = (v, g)_{H^{1}}$ for every $v \in H_{0}^{1} (Ω)$ , and $∥ g ∥_{H^{1}} = ∥ G ∥ = ∥ F ∥_{H^{- 1}}$ . Conjugating and expanding the $H^{1}$ inner product gives, for every $v$ , $F (v) = \overline{(v, g)_{H^{1}}} = (g, v)_{L^{2}} + \sum_{i = 1}^{n} (D_{i} g, D_{i} v)_{L^{2}},$ so with $f_{0} : = g$ and $f_{i} : = D_{i} g \in L^{2} (Ω)$ this is a representation of the required form.

3.1F1F3step 2.1step 1.2algebra∎

The canonical representation attains the infimum: for $f_{0} = g$ , $f_{i} = D_{i} g$ one has $\sum_{i = 0}^{n} ∥ f_{i} ∥_{L^{2}}^{2} = ∥ g ∥_{L^{2}}^{2} + \sum_{i} ∥ D_{i} g ∥_{L^{2}}^{2} = ∥ g ∥_{H^{1}}^{2} = ∥ F ∥_{H^{- 1}}^{2}$ by step 2.1, so the infimum is at most $∥ F ∥_{H^{- 1}}$ and, with step 1.2, equals it. The data of the canonical representation are controlled by the norm through $∥ g ∥_{H^{1}} = ∥ F ∥_{H^{- 1}}$ and conversely by the estimate of step 1.2. The construction uses Riesz representation in $H_{0}^{1}$ only; no Hahn--Banach extension is invoked.

Depends on

Used by

The weak Dirichlet Poisson problem on an interval Example

Dependency tree · two levels

78 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

John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)

Every H−1H−1 functional is an L2L2 function plus a divergence