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.

$L^{2}$ forcing and divergence data embed in $H^{- 1}$ with a quantitative bound

Statement

Assume the Axiom of Choice, inherited through the Poincar'e supplier named below, together with Countable Choice. Let $Ω \subseteq R^{n}$ be open, nonempty, bounded in one direction (so the Poincar'e inequality of The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction holds; every bounded open set qualifies), and let $f_{0}, f_{1}, \dots, f_{n} \in L^{2} (Ω; K)$ . Define $F (v) : = (f_{0}, v)_{L^{2}} + \sum_{i = 1}^{n} (f_{i}, D_{i} v)_{L^{2}}, v \in H_{0}^{1} (Ω),$ with the $L^{2}$ inner product of $L^{2}$ with the integral pairing is a Hilbert space. Then $F$ is a well-defined conjugate-linear functional on $H_{0}^{1} (Ω)$ , independent of the $L^{2}$ classes chosen only through those classes, and bounded: with the Poincar'e constant $C_{P}$ of $Ω$ for $W_{0}^{1, 2}$ , $∣ F (v) ∣ \leq (C_{P} ∥ f_{0} ∥_{L^{2}} + \sum_{i = 1}^{n} ∥ f_{i} ∥_{L^{2}}) ∥ v ∥_{H_{0}^{1}}, ∥ F ∥_{H^{- 1}} \leq C_{P} ∥ f_{0} ∥_{L^{2}} + \sum_{i = 1}^{n} ∥ f_{i} ∥_{L^{2}} .$ In particular $F \in H^{- 1} (Ω)$ in the sense of The negative Sobolev space $H^{- 1} (Ω)$ , and if $Ω$ is bounded then every $f \in L^{2} (Ω)$ defines an $H^{- 1}$ element by $v \mapsto (f, v)_{L^{2}}$ . The functional is the weak form of $f_{0} - \sum_{i} D_{i} f_{i}$ ; no claim that every $H^{- 1}$ element arises this way is made here.

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; an open, nonempty $Ω \subseteq R^{n}$ bounded in one direction, with a unit vector $e$ and reals $a < b$ such that $a < x \cdot e < b$ for all $x \in Ω$ ; classes $f_{0}, f_{1}, \dots, f_{n} \in L^{2} (Ω; K)$ ; and the functional $F (v) = (f_{0}, v)_{L^{2}} + \sum_{i = 1}^{n} (f_{i}, D_{i} v)_{L^{2}}$ on $H_{0}^{1} (Ω)$ .

[F1]

$H^{- 1} (Ω)$ is the space of bounded conjugate-linear functionals on $H_{0}^{1} (Ω)$ with $∥ F ∥_{H^{- 1}} = \sup_{∥ v ∥_{H_{0}^{1}} \leq 1} ∣ F (v) ∣$ ; the pairing $⟨ F, v ⟩ = F (v)$ is linear in $F$ and conjugate-linear in $v$ (The negative Sobolev space $H^{- 1} (Ω)$ , The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F2]

$H_{0}^{1} (Ω) = W_{0}^{1, 2} (Ω; K)$ carries the $W^{1, 2}$ norm, for which $∥ v ∥_{L^{2}} \leq ∥ v ∥_{H_{0}^{1}}$ , $∥ D_{i} v ∥_{L^{2}} \leq ∥ v ∥_{H_{0}^{1}}$ , and $∥ D v ∥_{L^{2}} = (\sum_{i = 1}^{n} ∥ D_{i} v ∥_{L^{2}}^{2})^{1 / 2}$ satisfies $∥ D v ∥_{L^{2}} \leq ∥ v ∥_{H_{0}^{1}}$ ; the weak derivatives are class operators in the sense of Weak derivative of a locally integrable function (Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure).

[F3]

Poincar'e inequality: with $C_{P} : = C (2) (b - a)$ for the constant of the cited theorem, $∥ v ∥_{L^{2} (Ω)} \leq C_{P} ∥ D v ∥_{L^{2} (Ω)}$ for every $v \in H_{0}^{1} (Ω)$ . This is the claim of The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction at $p = 2$ , stated there for $W_{0}^{1, p}$ classes.

[F4]

H"older and the $L^{2}$ pairing: $∣ (f, v)_{L^{2}} ∣ \leq ∥ f ∥_{L^{2}} ∥ v ∥_{L^{2}}$ for classes, the pairing is conjugate-linear in its second argument, and it depends only on the two classes (Holder's inequality for integrals, including the endpoint cases, The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions).

[F5]

The Axiom of Choice supplies Countable Choice for the Sobolev and $L^{2}$ interfaces (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F6]

$L^{2}$ functions are locally integrable by H"older on compact sets; they define regular distributions, whose coordinate derivatives satisfy $⟨ \partial_{i} u_{f}, φ ⟩ = - \int f D_{i} φ$ (Locally integrable functions embed in distributions, Regular distribution from a locally integrable function, Distributional derivative).

Proof

1.1F2F4

$F$ is well defined and conjugate-linear. Each summand $v \mapsto (f_{i}, D_{i} v)_{L^{2}}$ is a composition of the class map $v \mapsto D_{i} v$ , which is linear on Sobolev classes, with the $L^{2}$ pairing, which is conjugate-linear in its second argument; hence each summand is conjugate-linear and depends only on the class of $v$ and the class of $f_{i}$ . A finite sum of conjugate-linear functionals is conjugate-linear, so $F$ is a well-defined conjugate-linear functional on $H_{0}^{1} (Ω)$ .

2.1F1F2F3F4F5step 1.1algebra

Bound. For every $v \in H_{0}^{1} (Ω)$ , H"older gives $∣ (f_{0}, v)_{L^{2}} ∣ \leq ∥ f_{0} ∥_{L^{2}} ∥ v ∥_{L^{2}} \leq C_{P} ∥ f_{0} ∥_{L^{2}} ∥ D v ∥_{L^{2}}$ and $∣ (f_{i}, D_{i} v)_{L^{2}} ∣ \leq ∥ f_{i} ∥_{L^{2}} ∥ D_{i} v ∥_{L^{2}}$ for each $i$ ; summing and using $∥ D v ∥_{L^{2}} \leq ∥ v ∥_{H_{0}^{1}}$ and $∥ D_{i} v ∥_{L^{2}} \leq ∥ v ∥_{H_{0}^{1}}$ gives $∣ F (v) ∣ \leq (C_{P} ∥ f_{0} ∥_{L^{2}} + \sum_{i = 1}^{n} ∥ f_{i} ∥_{L^{2}}) ∥ v ∥_{H_{0}^{1}} .$ Consequently $F$ is bounded with $∥ F ∥_{H^{- 1}} \leq C_{P} ∥ f_{0} ∥_{L^{2}} + \sum_{i} ∥ f_{i} ∥_{L^{2}}$ , so $F \in H^{- 1} (Ω)$ .

3.1F3step 2.1

The pure $L^{2}$ case: if $Ω$ is bounded, then it is bounded in one direction --- for any unit vector $e$ and any $r$ with $Ω \subseteq B (0, r)$ one has $- r < x \cdot e < r$ --- so the hypothesis holds and $F (v) : = (f_{0}, v)_{L^{2}}$ with $f_{1} = \dots = f_{n} = 0$ is an element of $H^{- 1} (Ω)$ with $∥ F ∥_{H^{- 1}} \leq C_{P} ∥ f_{0} ∥_{L^{2}}$ .

4.1F2F4F6step 2.1∎

Identification with the divergence-form datum: let $u_{f_{i}}$ be the regular distribution associated to $f_{i} \in L^{2} \subset L_{l o c}^{1}$ and put $T : = u_{f_{0}} - \sum_{i} \partial_{i} u_{f_{i}}$ . For $v \in C_{c}^{\infty} (Ω)$ , the definition of the distributional derivative gives $⟨ T, \overline{v} ⟩ = \int f_{0} \overline{v} + \sum_{i} \int f_{i} \overline{D_{i} v} = F (v)$ . Thus $F$ extends this conjugated test pairing boundedly to $H_{0}^{1} (Ω)$ ; no function-valued derivative of any $f_{i}$ is assumed. The representation by data $(f_{0}, \dots, f_{n})$ is not asserted to be unique and no surjectivity onto $H^{- 1} (Ω)$ is claimed.

Remarks

The converse representation is proved in Every $H^{- 1}$ functional is an $L^{2}$ function plus a divergence.

Depends on

Used by

Dependency tree · two levels

83 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)
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)

L2L2 forcing and divergence data embed in H−1H−1 with a quantitative bound