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

The Dirichlet principle for the Poisson equation

Statement

Assume the Axiom of Choice (The Axiom of Choice), the ultrafilter lemma, DC and HB. Let $Ω \subseteq R^{n}$ , $n \geq 2$ , be a bounded $C^{1}$ domain, let $f \in L^{2} (Ω)$ and let $g \in H^{1 / 2} (\partial Ω) = W^{1 / 2, 2} (\partial Ω)$ lie in the trace range of $T : H^{1} (Ω) \to H^{1 / 2} (\partial Ω)$ (The sharp trace theorem: boundedness and range in the fractional space, The fractional Sobolev space on a compact $C^{1}$ boundary). Put $I (u) = \frac{1}{2} \int_{Ω} ∣ D u ∣^{2} d x - \int_{Ω} f u d x, K_{g} = {u \in H^{1} (Ω) : T u = g} .$ Then: (i) $I$ is strictly convex, coercive and weakly sequentially lower semicontinuous on $K_{g}$ (Convex and strictly convex functionals on a convex subset of a real vector space, Proper, coercive and weakly lower semicontinuous extended-real functionals), and attains its infimum at exactly one $u_{0} \in K_{g}$ (The direct method for convex integral functionals, Strict convexity gives uniqueness of a minimiser); (ii) $u_{0}$ is the unique weak solution of the Poisson problem $- Δ u = f$ with trace $g$ in the sense of Weak Dirichlet solutions for a divergence-form operator, so that $\int_{Ω} D u_{0} \cdot D φ d x = \int_{Ω} f φ d x$ for every $φ \in H_{0}^{1} (Ω)$ (The weak Euler-Lagrange equation for integral functionals with fixed trace, Existence and uniqueness for the weak Dirichlet Poisson problem, The inhomogeneous weak Dirichlet problem by a trace lifting); (iii) the classical one-directional Dirichlet principle holds: if $v \in C^{2} (\overline{Ω})$ satisfies $- Δ v = f$ in $Ω$ and $v ∣_{\partial Ω} = g$ , then $I (v) \leq I (w)$ for every $w \in K_{g}$ (First Green identity, Classical solutions satisfy the weak formulation).

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice), the ultrafilter lemma, DC and HB; a bounded $C^{1}$ domain $Ω \subseteq R^{n}$ , $n \geq 2$ ; $f \in L^{2} (Ω)$ ; $g \in H^{1 / 2} (\partial Ω)$ in the trace range of $T : H^{1} (Ω) \to H^{1 / 2} (\partial Ω)$ with affine class $K_{g}$ ; and the energy $I (u) = \frac{1}{2} \int_{Ω} ∣ D u ∣^{2} d x - \int_{Ω} f u d x$ .

[F0]

The Axiom of Choice is explicitly assumed here because the trace, trace-kernel and weak-Poisson suppliers used below state their conclusions under AC (The Axiom of Choice).

[F1]

The trace operator $T$ is bounded with $T u = u ∣_{\partial Ω}$ for continuous $u$ , and $H^{1 / 2} (\partial Ω) = W^{1 / 2, 2} (\partial Ω)$ (The $L^{p}$ trace operator on a bounded $C^{1}$ domain, The sharp trace theorem: boundedness and range in the fractional space, The fractional Sobolev space on a compact $C^{1}$ boundary).

[F2]

$K_{g}$ is nonempty, convex and weakly closed, and equals $R g + H_{0}^{1} (Ω)$ for any right inverse $R$ (The affine Dirichlet trace class is nonempty, convex and weakly closed); $\ker T = H_{0}^{1} (Ω)$ (The kernel of the trace is the closure of the test functions, Zero-boundary Sobolev space as a norm closure).

[F3]

The direct method for convex integral functionals: with $p = 2$ , a Caratheodory integrand convex and lower semicontinuous in $(s, ξ)$ satisfying the upper growth bound with $G \in L^{1} (Ω)$ and the coercivity bound holds, the functional attains its infimum on $K_{g}$ ; if the integrand satisfies the differentiation hypotheses, every minimiser solves the weak Euler-Lagrange equation, and strict convexity of the integrand in $(s, ξ)$ makes the minimiser unique (The direct method for convex integral functionals, The weak Euler-Lagrange equation for integral functionals with fixed trace, Strict convexity gives uniqueness of a minimiser).

[F4]

The weak Dirichlet solution of $- Δ u = f$ with trace $g$ is a class $u \in H^{1} (Ω)$ with $T u = g$ and $\int_{Ω} D u \cdot D φ = \int_{Ω} f φ$ for every $φ \in H_{0}^{1} (Ω)$ (Weak Dirichlet solutions for a divergence-form operator); such a solution exists and is unique, and agrees with the lifting construction (Existence and uniqueness for the weak Dirichlet Poisson problem, The inhomogeneous weak Dirichlet problem by a trace lifting).

[F5]

Poincare's inequality on $H_{0}^{1} (Ω)$ with constant $C_{P}$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction); $H^{1} (Ω) = W^{1, 2} (Ω)$ carries the Sobolev norm and inner product (The notation $H^{k}$ and the reserved zero-boundary symbol, Integer-order Sobolev spaces and their norms, The Sobolev space $H^{1}$ is a Hilbert space).

[F6]

If $v \in C^{2} (\overline{Ω})$ satisfies $- Δ v = f$ almost everywhere, first Green identity with $φ \in C_{c}^{\infty} (Ω)$ gives $\int_{Ω} D v \cdot D φ = \int_{Ω} f φ$ because the boundary test vanishes (First Green identity). Holder bounds both pairings by a constant times $∥ φ ∥_{H^{1}}$ , so density extends this identity to $H_{0}^{1} (Ω)$ (Holder's inequality for integrals, including the endpoint cases, Zero-boundary Sobolev space as a norm closure). This does not require the classical solution itself to have zero trace; the zero-trace-only supplier Classical solutions satisfy the weak formulation is therefore not applied to $v$ .

[F7]

The basic definitions: convex and strictly convex functionals, proper coercive weakly lower semicontinuous functionals (Convex and strictly convex functionals on a convex subset of a real vector space, Proper, coercive and weakly lower semicontinuous extended-real functionals).

Proof

technique · direct, by checking the hypotheses of the convex direct method for the Dirichlet integrand

1.1F5F7givenalgebra

The integrand and its bounds. Put $f_{0} (x, s, ξ) : = \frac{1}{2} ∣ ξ ∣^{2} - f (x) s$ . It is a Caratheodory integrand, jointly convex and continuous in $(s, ξ)$ , and the elementary inequality $∣ f (x) s ∣ \leq \frac{1}{2} ∣ f (x) ∣^{2} + \frac{1}{2} ∣ s ∣^{2}$ gives the upper bound $f_{0} \leq \frac{1}{2} (1 + ∣ s ∣^{2} + ∣ ξ ∣^{2}) + \frac{1}{2} ∣ f (x) ∣^{2}$ , admissible with $p = 2$ , $C = \frac{1}{2}$ and $G = \frac{1}{2} ∣ f ∣^{2} \in L^{1} (Ω)$ .

1.2F5givenalgebra

The coercivity bound with the smallness condition. Fix $ε > 0$ with $2 ε C_{P}^{2} \leq \frac{1}{8}$ ; Cauchy's inequality $∣ f (x) s ∣ \leq ε ∣ s ∣^{2} + \frac{1}{4 ε} ∣ f (x) ∣^{2}$ gives $f_{0} (x, s, ξ) \geq \frac{1}{2} ∣ ξ ∣^{2} - ε ∣ s ∣^{2} - \frac{1}{4 ε} ∣ f (x) ∣^{2}$ , which is the coercivity bound with $ν = \frac{1}{2}$ , $c = ε$ , $q = p = 2$ and $h = \frac{1}{4 ε} ∣ f ∣^{2} \geq 0$ , $h \in L^{1} (Ω)$ ; the smallness condition $2^{p - 1} c C_{P}^{p} = 2 ε C_{P}^{2} \leq \frac{1}{8} = ν \cdot 2^{- p}$ holds by the choice of $ε$ .

2.1F3F2F0step 1.1step 1.2

The direct method applies. By steps 1.1 and 1.2 the integrand satisfies all hypotheses of [F3] with $p = 2$ ; the class $K_{g}$ is nonempty, convex and weakly closed by [F2]; hence $I$ attains its infimum at some $u_{0} \in K_{g}$ , is coercive and weakly sequentially lower semicontinuous on $K_{g}$ .

3.1F2F3F5F7F0step 2.1algebra

Strict convexity of $I$ on $K_{g}$ . The functional is $I = Q - L$ with $Q (u) = \frac{1}{2} ∥ D u ∥_{2}^{2}$ and $L (u) = \int f u$ . The term $L$ is affine. The quadratic term $Q$ is strictly convex on $K_{g}$ : if $u \neq v$ in $K_{g}$ then $D (u - v)$ does not vanish almost everywhere, because $u - v \in H_{0}^{1} (Ω)$ by [F2], and Poincare [F5] would force $u - v = 0$ if $D (u - v) = 0$ ; consequently $Q (λ u + (1 - λ) v) < λ Q (u) + (1 - λ) Q (v)$ for $0 < λ < 1$ by the parallelogram identity. Hence $I$ is strictly convex on the convex set $K_{g}$ , and the minimiser $u_{0}$ of step 2.1 is unique by the strict-convexity uniqueness corollary Strict convexity gives uniqueness of a minimiser.

3.2F3F5F0step 2.1

The weak Euler-Lagrange equation. The integrand $f_{0}$ satisfies the differentiation hypotheses with $p = 2$ : $f_{0, s} = - f$ and $f_{0, ξ} = ξ$ are continuous in $(s, ξ)$ , $∣ f_{0} ∣ \leq \frac{1}{2} (1 + ∣ s ∣^{2} + ∣ ξ ∣^{2}) + \frac{1}{2} ∣ f ∣^{2}$ and $∣ f_{0, s} ∣ + ∣ f_{0, ξ} ∣ \leq (1 + ∣ s ∣ + ∣ ξ ∣) + ∣ f (x) ∣$ with $∣ f ∣ \in L^{2} (Ω) = L^{p^{'}} (Ω)$ . Hence the conditional clause of [F3] applies to the minimiser $u_{0}$ : $\int_{Ω} (D u_{0} \cdot D φ - f (x) φ) d x = 0$ for every $φ \in H_{0}^{1} (Ω)$ , that is $\int_{Ω} D u_{0} \cdot D φ = \int_{Ω} f φ$ .

4.1F4F0step 2.1step 3.1step 3.2

Identification with the weak Dirichlet solution. By steps 2.1 and 3.2 the minimiser $u_{0} \in H^{1} (Ω)$ satisfies $T u_{0} = g$ and $\int_{Ω} D u_{0} \cdot D φ = \int_{Ω} f φ$ for every $φ \in H_{0}^{1} (Ω)$ ; this is exactly the weak Dirichlet solution of $- Δ u = f$ with trace $g$ in the sense of [F4], and by the uniqueness statement of [F4] it is the unique such solution. This proves (i) and (ii).

5.1F1F2F5F6F0step 4.1∎

The classical one-directional principle. Let $v \in C^{2} (\overline{Ω})$ satisfy $- Δ v = f$ in $Ω$ and $v ∣_{\partial Ω} = g$ . Then $T v = g$ by [F1] (the trace restricts continuous functions pointwise), so for every $w \in K_{g}$ the difference $η : = w - v$ has $T η = 0$ , that is $η \in H_{0}^{1} (Ω)$ by [F2]. By [F6], applied to the classical solution $v$ , one has $\int_{Ω} D v \cdot D η = \int_{Ω} f η$ . Expanding the energy, $I (w) - I (v) = \frac{1}{2} \int_{Ω} (∣ D w ∣^{2} - ∣ D v ∣^{2}) d x - \int_{Ω} f η d x = \frac{1}{2} \int_{Ω} ∣ D η ∣^{2} d x + \int_{Ω} D v \cdot D η d x - \int_{Ω} f η d x = \frac{1}{2} \int_{Ω} ∣ D η ∣^{2} d x \geq 0$ , with equality if and only if $D η = 0$ almost everywhere, that is $w = v$ by [F5]. Hence $I (v) \leq I (w)$ for every $w \in K_{g}$ , the classical Dirichlet principle.

Depends on

Used by

Dependency tree · two levels

123 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 (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)
Viktor Grigoryan, Math 246B Partial Differential Equations, UCSB 2011 (complete 31-page course notes) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations, University of Illinois (complete 158-page graduate notes) (standard reference, not scraped)