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.

Minimisers are classical when elliptic regularity applies

Statement

Assume the Axiom of Choice and Countable Choice. Let $Ω \subseteq R^{n}$ , $n \geq 2$ , be a bounded domain, let $f$ and $g$ be given and let $u_{0} \in K_{g}$ be the minimiser of the Dirichlet energy of The Dirichlet principle for the Poisson equation. Then: (i) if $Ω$ is a bounded $C^{\infty}$ domain, $f$ extends to a $C^{\infty}$ function on a neighbourhood of $\overline{Ω}$ , and there is $G \in C^{\infty} (U)$ on a neighbourhood $U$ of $\overline{Ω}$ with $G ∣_{\partial Ω} = g$ , then $u_{0}$ agrees almost everywhere with a function $\tilde{u} \in C^{\infty} (\overline{Ω})$ satisfying $- Δ \tilde{u} = f$ pointwise in $Ω$ and $\tilde{u} = g$ on $\partial Ω$ (Smooth weak Dirichlet solutions are classical); (ii) if $0 < α < 1$ , $Ω$ is a bounded $C^{2, α}$ domain, $f \in C^{0, α} (\overline{Ω})$ and $g \in C^{2, α} (\overline{Ω})$ , then $u_{0} \in C^{2, α} (\overline{Ω})$ , $- Δ u_{0} = f$ pointwise and $u_{0} = g$ on $\partial Ω$ (Global Schauder regularity for the weak Dirichlet Laplacian). Variational existence alone gives only $u_{0} \in H^{1} (Ω)$ ; the smoothness asserted here is a consequence of elliptic regularity and fails without the corresponding hypotheses on the domain, coefficients and data.

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; a bounded domain $Ω \subseteq R^{n}$ , $n \geq 2$ ; data $f$ and $g$ ; and the minimiser $u_{0} \in K_{g}$ of the Dirichlet energy of The Dirichlet principle for the Poisson equation. In case (i), $Ω$ is a bounded $C^{\infty}$ domain, $f$ extends smoothly to a neighbourhood of $\overline{Ω}$ , and $G \in C^{\infty} (U)$ on a neighbourhood $U$ of $\overline{Ω}$ satisfies $G ∣_{\partial Ω} = g$ ; in case (ii) $0 < α < 1$ , $Ω$ is a bounded $C^{2, α}$ domain, $f \in C^{0, α} (\overline{Ω})$ and $g \in C^{2, α} (\overline{Ω})$ .

[F1]

The minimiser is the unique weak solution of $- Δ u = f$ with trace $g$ in the sense of Weak Dirichlet solutions for a divergence-form operator (The Dirichlet principle for the Poisson equation, The weak Euler-Lagrange equation for integral functionals with fixed trace).

[F2]

The trace of a smooth function is its boundary restriction, the kernel of the trace on a bounded $C^{1}$ domain is $H_{0}^{1}$ , and $H_{0}^{1}$ is the closure of $C_{c}^{\infty}$ (The trace agrees with classical restriction for continuous Sobolev functions, The kernel of the trace is the closure of the test functions, Zero-boundary Sobolev space as a norm closure).

[F3]

For $G \in C^{\infty} (U)$ and every $φ \in C_{c}^{\infty} (Ω)$ , classical integration by parts gives $\int_{Ω} D G \cdot D \overline{φ} d x = - \int_{Ω} (Δ G) \overline{φ} d x$ . Both functionals extend continuously to $H_{0}^{1} (Ω)$ because $D G \in L^{2}$ and $Δ G \in L^{2}$ on the bounded domain (Holder's inequality for integrals, including the endpoint cases).

[F4]

Smooth zero-boundary elliptic regularity: on a bounded $C^{\infty}$ domain, a zero-trace weak solution with smooth coefficients and forcing agrees almost everywhere with a $C^{\infty} (\overline{Ω})$ solution, satisfies the equation pointwise, and vanishes on the boundary (Smooth weak Dirichlet solutions are classical).

[F5]

Schauder regularity: if $0 < α < 1$ , $Ω$ is a bounded $C^{2, α}$ domain and the data are Holder, then the unique weak Dirichlet solution of $- Δ u = f$ lies in $C^{2, α} (\overline{Ω})$ , solves the equation pointwise and attains $g$ classically on $\partial Ω$ (Global Schauder regularity for the weak Dirichlet Laplacian).

Proof

technique · subtract a smooth boundary lift in the smooth case, then apply zero-boundary regularity; use the Schauder supplier directly in case (ii)

1.1F1given

The variational starting point. By [F1] the minimiser $u_{0}$ is the unique weak solution of $- Δ u = f$ with trace $g$ ; the variational analysis alone gives only $u_{0} \in H^{1} (Ω)$ , and no higher regularity is asserted by it.

1.2F1F2F3

Case (i): lift and zero trace. Let $G$ be the smooth extension in the hypothesis and set $v : = u_{0} - G$ . By [F1], $T u_{0} = g$ ; by [F2], $T G = G ∣_{\partial Ω} = g$ , so $T v = 0$ and the trace-kernel theorem gives $v \in H_{0}^{1} (Ω)$ . For every $φ \in C_{c}^{\infty} (Ω)$ , [F1] and [F3] give $\int_{Ω} D v \cdot D \overline{φ} d x = \int_{Ω} (f + Δ G) \overline{φ} d x .$ Both sides are continuous in the $H^{1}$ norm; density of $C_{c}^{\infty} (Ω)$ in $H_{0}^{1} (Ω)$ extends the identity to all $H_{0}^{1}$ tests. Thus $v$ is the zero-trace weak solution with smooth forcing $f + Δ G$ .

2.1F4step 1.2

Apply smooth regularity and restore the lift. The coefficients of $- Δ$ are smooth, and $f + Δ G$ extends smoothly to a neighbourhood of $\overline{Ω}$ . Supplier [F4] applies to $v$ , giving a smooth representative $\tilde{v} \in C^{\infty} (\overline{Ω})$ with $- Δ \tilde{v} = f + Δ G$ and $\tilde{v} = 0$ on $\partial Ω$ . Then $\tilde{u} : = \tilde{v} + G$ represents $u_{0}$ , satisfies $- Δ \tilde{u} = f$ pointwise and has boundary values $g$ .

2.2F1F5step 1.1

Case (ii). Under the Holder hypotheses of case (ii), [F5] applies to the same weak solution and yields $u_{0} \in C^{2, α} (\overline{Ω})$ with $- Δ u_{0} = f$ pointwise and $u_{0} = g$ on $\partial Ω$ .

3.1step 1.1step 2.1step 2.2∎

The warning. Both conclusions are consequences of elliptic regularity under the stated hypotheses on the domain, the coefficients and the data; without them variational existence alone gives only $u_{0} \in H^{1} (Ω)$ , as the companion counterexamples on weak solutions without higher regularity record.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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