CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Weak comparison and uniqueness for the Dirichlet problem

Statement

Assume Countable Choice and the Axiom of Choice. Let $n \geq 2$ , let $Ω \subset R^{n}$ be a bounded $C^{1}$ domain, and let $L, a$ be as in Weak subsolutions and supersolutions of a divergence-form equation with real $L^{\infty}$ coefficients, ellipticity $θ$ and bounds $M_{a}, M_{b}, M_{c}$ , satisfying $c \geq 0$ a.e. and the weak sign condition of Weak maximum principle for coercive divergence-form equations. Let $f \in L_{l o c}^{1} (Ω)$ and let $u, v \in H^{1} (Ω; R)$ be a local weak subsolution resp. weak supersolution of $L u = f$ with $u \leq v$ on $\partial Ω$ , i.e. $(u - v)^{+} \in H_{0}^{1} (Ω)$ . Then $u \leq v$ a.e. on $Ω$ . Consequently:

if $b \equiv 0$ , $c \geq 0$ a.e. and $f \in L^{q} (Ω)$ with $q > n / 2$ , then every weak solution of $L u = f$ with $u \leq 0$ on $\partial Ω$ satisfies ${ess sup}_{Ω} u \leq C ∥ f^{+} ∥_{L^{q} (Ω)}$ with the constant of Weak maximum principle for coercive divergence-form equations;
if $b \equiv 0$ , $c \geq 0$ a.e. and $f = 0$ , then two weak solutions of $L u = 0$ with the same trace in $H^{1 / 2} (\partial Ω)$ (Weak Dirichlet solutions for a divergence-form operator) agree a.e. on $Ω$ ; in particular the homogeneous Dirichlet problem has at most one weak solution for each admissible boundary datum.

Facts & Assumptions

Given: Countable Choice and the Axiom of Choice; a bounded $C^{1}$ domain $Ω \subset R^{n}$ , $n \geq 2$ ; real coefficients satisfying $c \geq 0$ and the weak-sign hypotheses of Weak maximum principle for coercive divergence-form equations; a datum $f \in L_{l o c}^{1} (Ω)$ ; and a local weak subsolution $u$ and local weak supersolution $v$ of $L u = f$ with $(u - v)^{+} \in H_{0}^{1} (Ω)$ .

[F1]

Linearity of the form: for every real nonnegative $φ \in C_{c}^{\infty} (Ω)$ , $a (u - v, φ) = a (u, φ) - a (v, φ)$ ; the form is the one of Uniformly elliptic divergence-form operators and their sesquilinear forms.

[F2]

Weak maximum principle: under $c \geq 0$ and the weak-sign condition, a real local weak subsolution $W \in H^{1} (Ω)$ of $L W = 0$ satisfies ${ess sup}_{Ω} W \leq \sup_{\partial Ω} W^{+}$ ; with $b = 0, c \geq 0$ and $g \in L^{q} (Ω)$ , $q > n / 2$ , a local subsolution with $W^{+} \in H_{0}^{1}$ satisfies ${ess sup}_{Ω} W \leq C ∥ g^{+} ∥_{L^{q}}$ (Weak maximum principle for coercive divergence-form equations).

[F3]

Boundary order and traces: $\sup_{\partial Ω} W = {ess sup}_{\partial Ω} T W$ , and $W^{+} \in H_{0}^{1} (Ω)$ implies $\sup_{\partial Ω} W^{+} = 0$ ; moreover $(u - v)^{+} \in H_{0}^{1} (Ω)$ is exactly the boundary inequality $u \leq v$ on $\partial Ω$ (A function whose trace is at most a level has positive part in the zero-boundary space, Weak subsolutions and supersolutions of a divergence-form equation, The kernel of the trace is the closure of the test functions).

Proof

technique · direct; apply the linearity of the form to the difference and invoke the weak maximum principle

1.1givenF1F3

The difference is a local weak subsolution of the homogeneous equation. Let $W : = u - v \in H^{1} (Ω; R)$ and let $φ \in C_{c}^{\infty} (Ω; R)$ be nonnegative. The local subsolution and supersolution inequalities give $a (u, φ) \leq \int_{Ω} f φ$ and $a (v, φ) \geq \int_{Ω} f φ$ , hence by [F1] $a (W, φ) \leq 0$ . Moreover $(u - v)^{+} = W^{+} \in H_{0}^{1} (Ω)$ by hypothesis, so $\sup_{\partial Ω} W^{+} = 0$ by [F3].

2.1step 1.1F2F3

Conclusion of the comparison. Step 1.1 exhibits $W$ as a weak subsolution of $L W = 0$ whose positive part lies in $H_{0}^{1} (Ω)$ ; [F2] gives ${ess sup}_{Ω} W \leq \sup_{\partial Ω} W^{+} = 0$ , that is, $u \leq v$ a.e. on $Ω$ .

3.1step 2.1F2F3

Consequence 1. If $b \equiv 0$ , $c \geq 0$ and $f \in L^{q} (Ω)$ with $q > n / 2$ , and $u$ is a weak solution with $u \leq 0$ on $\partial Ω$ , then $u$ is a weak subsolution of $L u = f$ and $u^{+} \in H_{0}^{1} (Ω)$ by the boundary hypothesis; the forcing clause of [F2] gives ${ess sup}_{Ω} u \leq C ∥ f^{+} ∥_{L^{q} (Ω)}$ with the constant recorded in Weak maximum principle for coercive divergence-form equations.

4.1step 2.1F3∎

Consequence 2 (uniqueness). Let $u, v$ be weak solutions of $L u = 0$ with the same trace in $H^{1 / 2} (\partial Ω)$ . Then $(u - v)^{+} \in H_{0}^{1} (Ω)$ and $(v - u)^{+} \in H_{0}^{1} (Ω)$ because the traces agree (The kernel of the trace is the closure of the test functions), so step 2.1 applied to the pair $(u, v)$ and to $(v, u)$ gives $u \leq v$ and $v \leq u$ a.e., i.e. $u = v$ a.e. Hence the homogeneous Dirichlet problem has at most one weak solution for each admissible boundary datum, and the comparison statement and its two consequences use only the declared choice principles.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (author manuscript, version 11 February 2025; complete 392-page archived text) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford University; complete author scan, 118 sheets reproducing the 223 printed pages of the manuscript, two logical pages per sheet) (standard reference, not scraped)