ExampleConstruction: Literature-sourcedVerification: 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 defines an $H^{- 1}$ functional

Example

Assume the Axiom of Choice inherited through the cited suppliers, together with Countable Choice. Let $Ω \subseteq R^{n}$ be open, nonempty and bounded in one direction, with Poincar'e constant $C_{P}$ for $W_{0}^{1, 2}$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction). For $f \in L^{2} (Ω)$ define $F_{f} (v) : = (f, v)_{L^{2}}$ , $v \in H_{0}^{1} (Ω)$ . Then $F_{f} \in H^{- 1} (Ω)$ (The negative Sobolev space $H^{- 1} (Ω)$ ) with $∥ F_{f} ∥_{H^{- 1}} \leq C_{P} ∥ f ∥_{L^{2}} .$ If moreover $f \in H_{0}^{1} (Ω)$ and $f \neq 0$ , testing $v = f$ gives the data-dependent lower bound $∥ F_{f} ∥_{H^{- 1}} \geq \frac{∥ f ∥_{L^{2}}^{2}}{∥ f ∥_{H_{0}^{1}}};$ no uniform positive lower bound by $∥ f ∥_{L^{2}}$ holds on all of $H_{0}^{1}$ , as the interval sine sequence below shows. The map $f \mapsto F_{f}$ is injective: if $F_{f} = 0$ then $(f, v)_{L^{2}} = 0$ for all $v \in C_{c}^{\infty} (Ω)$ , hence $f = 0$ a.e. Taking $f = 1$ on a bounded interval $(0, L)$ shows that the upper bound $C_{P} ∥ f ∥_{L^{2}}$ is at least $(L / π) \sqrt{L}$ there and grows with the domain diameter. This is the exact cheap estimate that the plan records as consumed by the weak Dirichlet problem ( $L^{2}$ forcing and divergence data embed in $H^{- 1}$ with a quantitative bound); it is not surjectivity of the embedding, which fails for $n \geq 1$ (an explicit datum outside its range is constructed in step 1.4; Every $H^{- 1}$ functional is an $L^{2}$ function plus a divergence supplies the general representation).

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; an open, nonempty $Ω \subseteq R^{n}$ bounded in one direction with Poincar'e constant $C_{P}$ for $W_{0}^{1, 2}$ ; a class $f \in L^{2} (Ω)$ ; the functional $F_{f} (v) = (f, v)_{L^{2}}$ on $H_{0}^{1} (Ω)$ .

[F1]

Upper estimate: the functional $v \mapsto (f, v)_{L^{2}}$ is conjugate-linear, well defined on classes, and $∥ F_{f} ∥_{H^{- 1}} \leq C_{P} ∥ f ∥_{L^{2}}$ ; this is $L^{2}$ forcing and divergence data embed in $H^{- 1}$ with a quantitative bound with $f_{0} = f$ and $f_{1} = \dots = f_{n} = 0$ , using $∥ v ∥_{L^{2}} \leq C_{P} ∥ D v ∥_{L^{2}}$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction).

[F2]

$H^{- 1}$ norm and the lower bound: $∥ F ∥_{H^{- 1}} = \sup_{∥ v ∥_{H_{0}^{1}} \leq 1} ∣ F (v) ∣$ , so for $f \neq 0$ testing with $v = f \in H_{0}^{1}$ gives $∥ F_{f} ∥_{H^{- 1}} \geq ∣ (f, f)_{L^{2}} ∣ / ∥ f ∥_{H_{0}^{1}} = ∥ f ∥_{L^{2}}^{2} / ∥ f ∥_{H_{0}^{1}}$ . Poincar'e controls $∥ f ∥_{L^{2}}$ by $∥ D f ∥_{L^{2}}$ and supplies no upper bound of $∥ f ∥_{H_{0}^{1}}$ by $∥ f ∥_{L^{2}}$ (The negative Sobolev space $H^{- 1} (Ω)$ , Integer-order Sobolev spaces and their norms, The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction, Zero-boundary Sobolev space as a norm closure).

[F3]

Injectivity input: the map $f \mapsto u_{f}$ , $u_{f} (φ) = \int_{Ω} f φ$ , is an injection from $L_{l o c}^{1} (Ω)$ modulo almost-everywhere equality into the distributions $D^{'} (Ω)$ , $D^{'} (Ω)$ being the continuous linear functionals on the test-function space $D (Ω) = C_{c}^{\infty} (Ω)$ ; hence $u_{f} = 0$ forces $f = 0$ a.e. (Locally integrable functions embed in distributions, Regular distribution from a locally integrable function, Test function space d of an open set). Every $L^{2}$ class on $Ω$ lies in $L_{l o c}^{1} (Ω)$ , because $\int_{K} ∣ f ∣ \leq ∣ K ∣^{1 / 2} ∥ f ∥_{L^{2} (K)}$ on each compact $K \subseteq Ω$ (Holder's inequality for integrals, including the endpoint cases).

[F4]

Sharp interval inequality: on $Ω = (0, L)$ the function $ϕ (x) = \sin (π x / L)$ lies in $H_{0}^{1} (0, L)$ , is nonzero, and satisfies $∥ ϕ ∥_{L^{2}} = (L / π) ∥ ϕ^{'} ∥_{L^{2}}$ , so every constant $C$ admissible in $∥ v ∥_{L^{2}} \leq C ∥ \nabla v ∥_{L^{2}}$ on $H_{0}^{1} (0, L)$ satisfies $C \geq L / π$ (The sharp Dirichlet Poincare inequality on an interval).

[F5]

The constant function $1$ on $(0, L)$ has $∥ 1 ∥_{L^{2} (0, L)} = \sqrt{L}$ : the constant $1$ is bounded and Riemann integrable on $[0, L]$ with Riemann integral $L$ , and a bounded Riemann integrable function on a closed bounded interval has the same Lebesgue integral (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ , A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral, The space $L^{p} (μ)$ as the quotient by null functions, Integral over a measurable subset).

[F6]

For integers $k \geq 1$ , $f_{k} (x) = \sin (k π x)$ on $(0, 1)$ satisfies $∥ f_{k} ∥_{L^{2}}^{2} = 1 / 2$ , $∥ f_{k}^{'} ∥_{L^{2}}^{2} = (k π)^{2} / 2$ , and $f_{k}^{''} = - (k π)^{2} f_{k}$ by the trigonometric identities and derivative rules (The derivatives of sine and cosine are cosine and minus sine, The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine, 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)$ ).

[F7]

The standard smooth step $σ$ takes values in $[0, 1]$ , equals $0$ on $(- \infty, 0]$ and $1$ on $[1, \infty)$ , and has bounded derivative $C_{σ} : = \sup ∣ σ^{'} ∣ < \infty$ because $σ^{'}$ is continuous and vanishes outside the compact interval $[0, 1]$ (The standard smooth step function, Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value).

[F8]

Integration by parts applies to smooth compactly supported test functions on $I$ , and $C_{c}^{\infty} (I)$ is dense in $H_{0}^{1} (I)$ by its definition as a Sobolev closure; the pairings in the identity are continuous in the $H_{0}^{1}$ norm (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ , Zero-boundary Sobolev space as a norm closure, Holder's inequality for integrals, including the endpoint cases).

[F9]

Arbitrary $L^{2}$ data $f_{0}, \dots, f_{n}$ define a bounded functional $F (v) = (f_{0}, v) + \sum_{i} (f_{i}, D_{i} v)$ by $L^{2}$ forcing and divergence data embed in $H^{- 1}$ with a quantitative bound. Smooth compactly supported bumps exist inside every ball, by A smooth bump between concentric Euclidean balls and translation; their products give bumps inside boxes. Fubini factors integrals of products on boxes (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability), and the fundamental theorem evaluates the smooth one-variable derivative integrals (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

Proof

1.1F1

Upper bound: [F1] applied with $f_{0} = f$ and all $f_{i} = 0$ gives $∥ F_{f} ∥_{H^{- 1}} \leq C_{P} ∥ f ∥_{L^{2}}$ , so $F_{f} \in H^{- 1} (Ω)$ .

1.2F2

Exact lower bound on the Sobolev space: if $f \in H_{0}^{1} (Ω)$ is nonzero, then $f$ is an admissible test function and $\frac{∣ F_{f} (f) ∣}{∥ f ∥_{H_{0}^{1}}} = \frac{∥ f ∥_{L^{2}}^{2}}{∥ f ∥_{H_{0}^{1}}}$ is a lower bound for $∥ F_{f} ∥_{H^{- 1}}$ , because that norm is the supremum of $∣ F_{f} (v) ∣ / ∥ v ∥_{H_{0}^{1}}$ over nonzero $v$ .

1.3F4F5algebra

Interval scaling: take $Ω = (0, L)$ and $f = 1$ . By the sharp interval inequality every admissible Poincar'e constant $C$ for $(0, L)$ satisfies $C \geq L / π$ , and $∥ f ∥_{L^{2} (0, L)} = \sqrt{L}$ ; hence the displayed bound $C_{P} ∥ f ∥_{L^{2}}$ is at least $(L / π) \sqrt{L}$ and grows with the diameter $L$ of the domain.

1.4F1F9algebra

The embedding is not onto. Choose a box $Q = (s - r, s + r) \times Q^{'}$ compactly contained in the nonempty open set $Ω$ , a real $ψ \in C_{c}^{\infty} (- 1, 1)$ with $ψ (0) = 1$ , and a nonzero real $η \in C_{c}^{\infty} (Q^{'})$ using [F9]. For $n = 1$ , omit the transverse factor and set $C = 1$ ; otherwise put $C : = \int_{Q^{'}} η^{2} > 0$ . Set $f_{1} (x) = 1_{(s, s + r)} (x_{1}) η (x^{'})$ on $Q$ and zero outside, with $f_{0} = f_{2} = \dots = f_{n} = 0$ . These are $L^{2}$ data, so $F (v) : = \int f_{1} \overline{D_{1} v}$ belongs to $H^{- 1}$ by [F9]. For $0 < ε < r$ , take $v_{ε} (x) = ψ ((x_{1} - s) / ε) η (x^{'}) \in C_{c}^{\infty} (Q)$ . Fubini and the fundamental theorem give $F (v_{ε}) = C (ψ (r / ε) - ψ (0)) = - C$ , whereas $∥ v_{ε} ∥_{2}^{2} = ε C \int_{- 1}^{1} ψ^{2} \to 0$ . If $F = F_{h}$ for some $h \in L^{2} (Ω)$ , H"older would imply $∣ F (v_{ε}) ∣ \leq ∥ h ∥_{2} ∥ v_{ε} ∥_{2} \to 0$ , contradicting $C > 0$ . Thus a datum outside the $L^{2}$ embedding exists on every such nonempty $Ω$ .

2.1F2F6F7F8step 1.1algebra

No uniform $L^{2}$ lower bound: on $I = (0, 1)$ , let $f_{k} (x) = \sin (k π x)$ . To see $f_{k} \in H_{0}^{1} (I)$ , for each fixed $k$ use $η_{m} (x) = σ (m x - 1) σ (m (1 - x) - 1)$ and set $g_{k, m} = η_{m} f_{k}$ . Then $g_{k, m} \in C_{c}^{\infty} (I)$ , $η_{m} = 1$ on $[2 / m, 1 - 2 / m]$ , $∣ η_{m}^{'} ∣ \leq 2 m C_{σ}$ , and on the two boundary strips $∣ f_{k} ∣ \leq 2 k π / m$ and $∣ f_{k}^{'} ∣ \leq k π$ . Thus $∥ g_{k, m} - f_{k} ∥_{L^{2}}^{2} \leq 16 (k π)^{2} / m^{3}$ and $∥ (g_{k, m} - f_{k})^{'} ∥_{L^{2}}^{2} \leq 4 (k π)^{2} (1 + 4 C_{σ})^{2} / m$ , so $g_{k, m} \to f_{k}$ in $H^{1}$ and $f_{k} \in H_{0}^{1} (I)$ . By [F8], first for $v \in C_{c}^{\infty} (I)$ and then by density for every $v \in H_{0}^{1} (I)$ , $F_{f_{k}} (v) = \int_{0}^{1} f_{k} \overline{v} d x = \frac{1}{(k π)^{2}} \int_{0}^{1} f_{k}^{'} \overline{v^{'}} d x .$ Cauchy--Schwarz and [F6] give $∥ F_{f_{k}} ∥_{H^{- 1}} \leq ∥ f_{k} ∥_{L^{2}} / (k π)$ , so $∥ F_{f_{k}} ∥_{H^{- 1}} / ∥ f_{k} ∥_{L^{2}} \to 0$ . Therefore no uniform positive lower bound by $∥ f ∥_{L^{2}}$ holds on all of $H_{0}^{1} (I)$ .

3.1F3step 1.1step 1.2step 2.1

Injectivity: if $F_{f} = 0$ , then $(f, v)_{L^{2}} = 0$ for every $v \in C_{c}^{\infty} (Ω) \subseteq H_{0}^{1} (Ω)$ . Given $φ \in C_{c}^{\infty} (Ω)$ , applying this to $v = \overline{φ}$ gives $u_{f} (φ) = \int_{Ω} f φ = 0$ , so $u_{f}$ is the zero distribution; the injectivity in [F3] then gives $f = 0$ a.e., that is, $f$ is the zero class. Hence $f \mapsto F_{f}$ is injective. When $f \in H_{0}^{1} (Ω)$ , steps 1.1 and 1.2 give an upper bound and the valid data-dependent lower bound; step 2.1 shows that this lower bound cannot be replaced by a uniform positive multiple of $∥ f ∥_{L^{2}}$ .

4.1F1step 2.1step 3.1step 1.4step 1.3step 1.2∎

Conclusion: $L^{2}$ forcing defines an element of $H^{- 1}$ with the quantitative upper bound of step 1.1, the valid data-dependent lower bound of step 1.2 for $f \in H_{0}^{1}$ , injectivity by step 3.1, and diameter growth of the upper bound by step 1.3. Step 2.1 shows why there is no uniform lower estimate in the $L^{2}$ norm; this example is not surjectivity of $L^{2} (Ω) ↪ H^{- 1} (Ω)$ , as the explicit datum of step 1.4 is outside its range.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

137 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)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (archived 2025 author manuscript) (standard reference, not scraped)

L2L2 forcing defines an H−1H−1 functional