LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Classical solutions satisfy the weak formulation

Statement

Assume the Axiom of Choice (through the published Sobolev Gauss--Green formula) and Countable Choice. Let $Ω \subset R^{n}$ , $n \geq 2$ , be a bounded $C^{1}$ domain, let $a^{i j} \in C^{1} (\overline{Ω})$ , $b^{i}, c \in C (\overline{Ω})$ with uniform ellipticity constant $θ$ (Uniformly elliptic divergence-form operators and their sesquilinear forms, Bounded C^k domains and boundary charts), let $u \in C^{2} (\overline{Ω}) \cap H_{0}^{1} (Ω)$ and $f \in C (\overline{Ω})$ , and set $L u : = - D_{i} (a^{i j} D_{j} u) + b^{i} D_{i} u + c u .$ If $L u = f$ on $Ω$ , then $u$ is a weak solution in the sense of Weak Dirichlet solutions for a divergence-form operator for the datum $F_{f} (v) : = (f, v)_{L^{2}}$ : $a (u, v) = \int_{Ω} f \overline{v} d x for every v \in H_{0}^{1} (Ω) .$ No converse is claimed: the lemma is the classical-to-weak consistency statement only.

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; a bounded $C^{1}$ domain $Ω \subset R^{n}$ , $n \geq 2$ ; coefficients $a^{i j} \in C^{1} (\overline{Ω})$ , $b^{i}, c \in C (\overline{Ω})$ with ellipticity constant $θ$ ; a class $u \in C^{2} (\overline{Ω}) \cap H_{0}^{1} (Ω)$ and $f \in C (\overline{Ω})$ with $L u : = - D_{i} (a^{i j} D_{j} u) + b^{i} D_{i} u + c u = f$ on $Ω$ ; the divergence form $a (u, v) = \int_{Ω} (a^{i j} D_{j} u \overline{D_{i} v} + b^{i} D_{i} u \overline{v} + c u \overline{v}) d x$ ; and the trace operator $T$ of The $L^{p}$ trace operator on a bounded $C^{1}$ domain with outward normal $ν$ .

[F1]

$u \in C^{2} (\overline{Ω}) \cap H_{0}^{1} (Ω)$ has classical derivatives that are its weak derivatives, and likewise $a^{i j} D_{j} u \in C^{1} (\overline{Ω})$ has for each $i$ the classical derivative $D_{i} (a^{i j} D_{j} u) \in C (\overline{Ω})$ as its weak derivative (Classical derivatives agree with weak derivatives, $C^{k}$ maps and multi-index derivative notation in Euclidean space, Uniformly elliptic divergence-form operators and their sesquilinear forms).

[F2]

Kernel of the trace: for $1 \leq p < \infty$ the kernel of $T$ on $W^{1, p} (Ω)$ is exactly $W_{0}^{1, p} (Ω)$ ; in particular $w \in H_{0}^{1} (Ω)$ implies $T w = 0$ (The kernel of the trace is the closure of the test functions, Zero-boundary Sobolev space as a norm closure).

[F3]

$H_{0}^{1} (Ω)$ is stable under conjugation, being the closure of the conjugation-stable space $C_{c}^{\infty} (Ω; K)$ ; complex weak derivatives are taken componentwise, so $D_{i} \overline{w} = \overline{D_{i} w}$ for $w \in H^{1}$ (Zero-boundary Sobolev space as a norm closure, Complex Lp classes and Euclidean test-function conventions, Integer-order Sobolev spaces and their norms).

[F4]

Sobolev Gauss--Green: for $n \geq 2$ , $1 < p < \infty$ , $U \in W^{1, p} (Ω; K)$ and $W \in W^{1, p^{'}} (Ω; K)$ one has $\int_{Ω} U D_{i} W d x = - \int_{Ω} (D_{i} U) W d x + \int_{\partial Ω} (T U) (T W) ν_{i} d S$ , all integrals finite (The Gauss-Green integration-by-parts formula with Sobolev traces, Bounded C^k domains and boundary charts, Classical normal derivative).

[F5]

The datum $F_{f} (v) : = (f, v)_{L^{2}}$ is a bounded conjugate-linear functional on $H_{0}^{1} (Ω)$ , i.e. an element of $H^{- 1} (Ω)$ : $∣ F_{f} (v) ∣ \leq ∥ f ∥_{L^{2}} ∥ v ∥_{L^{2}} \leq ∥ f ∥_{L^{2}} ∥ v ∥_{H_{0}^{1}}$ , and $Ω$ is bounded hence bounded in one direction ( $L^{2}$ forcing and divergence data embed in $H^{- 1}$ with a quantitative bound, Holder's inequality for integrals, including the endpoint cases, Weak Dirichlet solutions for a divergence-form operator, The space $L^{p} (μ)$ as the quotient by null functions).

Proof

1.1F2F3

Boundary term vanishes: let $v \in H_{0}^{1} (Ω)$ . Then $\overline{v} \in H_{0}^{1} (Ω)$ by conjugation stability, so $T \overline{v} = 0$ ; consequently every boundary term carrying the factor $T \overline{v}$ vanishes.

2.1F1F3F4step 1.1

Gauss--Green for one coefficient: fix $i$ . Since $a^{i j} D_{j} u \in C^{1} (\overline{Ω}) \subseteq W^{1, 2} (Ω)$ and $\overline{v} \in W^{1, 2} (Ω)$ , applying the Gauss--Green formula with $U = a^{i j} D_{j} u$ and $W = \overline{v}$ gives $\int_{Ω} a^{i j} D_{j} u \overline{D_{i} v} d x = - \int_{Ω} D_{i} (a^{i j} D_{j} u) \overline{v} d x + \int_{\partial Ω} T (a^{i j} D_{j} u) T (\overline{v}) ν_{i} d S,$ and the boundary integral is $0$ by step 1.1. Summing over $i, j$ and noting that $D_{i} \overline{v} = \overline{D_{i} v}$ and $D_{j} u$ are the weak derivatives of the classical ones yields $\int_{Ω} a^{i j} D_{j} u \overline{D_{i} v} d x = - \int_{Ω} D_{i} (a^{i j} D_{j} u) \overline{v} d x$ .

3.1F1F3step 2.1algebra

Weak equation: adding the drift and reaction terms and using the classical derivatives as weak derivatives, $a (u, v) = \int_{Ω} (- D_{i} (a^{i j} D_{j} u) + b^{i} D_{i} u + c u) \overline{v} d x = \int_{Ω} (L u) \overline{v} d x = \int_{Ω} f \overline{v} d x$ for every $v \in H_{0}^{1} (Ω)$ ; here $L u = f$ holds as an identity of continuous functions on $Ω$ by hypothesis, and $F_{f} (v) = \int_{Ω} f \overline{v} d x$ is the $L^{2}$ pairing.

4.1F5step 3.1∎

Conclusion: by [F5] the functional $F_{f}$ lies in $H^{- 1} (Ω)$ , and step 3.1 exhibits $a (u, v) = F_{f} (v)$ for every $v \in H_{0}^{1} (Ω)$ with $u \in C^{2} (\overline{Ω}) \cap H_{0}^{1} (Ω)$ ; hence every classical solution with $L u = f$ is a weak solution in the sense of the definition. No converse is claimed.

Depends on

Used by

The weak maximum principle needs the zero-order sign condition Counterexample
The weak and the classical maximum principles agree on a smooth subsolution Example
The Dirichlet principle for the Poisson equation Theorem

Dependency tree · two levels

95 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)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (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)